aboutsummaryrefslogtreecommitdiffhomepage
path: root/test/Solver
diff options
context:
space:
mode:
Diffstat (limited to 'test/Solver')
-rw-r--r--test/Solver/2016-04-12-array-parsing-bug.kquery227
1 files changed, 227 insertions, 0 deletions
diff --git a/test/Solver/2016-04-12-array-parsing-bug.kquery b/test/Solver/2016-04-12-array-parsing-bug.kquery
new file mode 100644
index 00000000..d53fa35f
--- /dev/null
+++ b/test/Solver/2016-04-12-array-parsing-bug.kquery
@@ -0,0 +1,227 @@
+# RUN: %kleaver %s > %t
+# RUN: %kleaver --clear-array-decls-after-query %s > %t
+
+array A-data[8] : w32 -> w8 = symbolic
+array A-data-stat[144] : w32 -> w8 = symbolic
+array arg0[3] : w32 -> w8 = symbolic
+array arg1[3] : w32 -> w8 = symbolic
+array const_arr1[768] : w32 -> w8 = [0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 3 32 2 32 2 32 2 32 2 32 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 2 0 1 96 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 4 192 8 216 8 216 8 216 8 216 8 216 8 216 8 216 8 216 8 216 8 216 4 192 4 192 4 192 4 192 4 192 4 192 4 192 8 213 8 213 8 213 8 213 8 213 8 213 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 8 197 4 192 4 192 4 192 4 192 4 192 4 192 8 214 8 214 8 214 8 214 8 214 8 214 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 8 198 4 192 4 192 4 192 4 192 2 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0]
+array const_arr8[277] : w32 -> w8 = [0 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 24 2 2 25 2 2 2 2 2 2 2 2 2 2 23 2 2 2 2 2 22 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21]
+array model_version[4] : w32 -> w8 = symbolic
+array n_args[4] : w32 -> w8 = symbolic
+array n_args_1[4] : w32 -> w8 = symbolic
+array stdin[8] : w32 -> w8 = symbolic
+array stdin-stat[144] : w32 -> w8 = symbolic
+array stdout[1024] : w32 -> w8 = symbolic
+array stdout-stat[144] : w32 -> w8 = symbolic
+(query [(Ult N0:(ReadLSB w32 0 n_args)
+ 2)
+ (Eq false (Slt 0 N0))
+ (Ult N1:(ReadLSB w32 0 n_args_1)
+ 3)
+ (Slt 0 N1)
+ (Slt 1 N1)
+ (Eq false
+ (Eq 0
+ (And w64 (ReadLSB w64 8 A-data-stat)
+ 2147483647)))
+ (Ult (ReadLSB w64 56 A-data-stat)
+ 65536)
+ (Eq false
+ (Eq 0
+ (And w64 (ReadLSB w64 8 stdin-stat)
+ 2147483647)))
+ (Ult (ReadLSB w64 56 stdin-stat)
+ 65536)
+ (Eq false
+ (Eq 0
+ (And w64 (ReadLSB w64 8 stdout-stat)
+ 2147483647)))
+ (Ult (ReadLSB w64 56 stdout-stat)
+ 65536)
+ (Eq 1
+ (ReadLSB w32 0 model_version))
+ (Eq 45 (Read w8 0 arg0))
+ (Eq false
+ (Eq 0 N2:(Read w8 1 arg0)))
+ (Eq false (Eq 45 N2))
+ (Eq 100
+ (AShr w32 (Shl w32 (SExt w32 N2) 24)
+ 24))
+ (Eq 0
+ (And w16 (ReadLSB w16 N3:(Extract w32 0 (Add w64 256
+ (Mul w64 2
+ (ZExt w64 N4:(Read w8 0 arg1))))) const_arr1)
+ 8192))
+ (Eq false (Eq 84 N4))
+ (Eq false
+ (Ult (Add w64 18446744073664565360
+ N5:(Select w64 (Eq 0 N4) 44986256 51741584))
+ 2))
+ (Eq false
+ (Ult (Add w32 4294967248
+ (ZExt w32 N6:(Read w8 (Extract w32 0 (Add w64 18446744073657810032 N5))
+ U0:[2=0] @ arg1)))
+ 10))
+ (Eq false (Eq 45 N6))
+ (Eq false (Eq 43 N6))
+ (Eq 0
+ (And w16 (ReadLSB w16 N7:(Extract w32 0 (Add w64 256
+ (Mul w64 2 (ZExt w64 N6)))) const_arr1)
+ 1024))
+ (Eq false (Eq 40 N6))
+ (Eq false
+ (Slt N8:(SExt w32 N6) 1))
+ (Ult 96
+ (Add w32 4294967286
+ (ZExt w32 (Read w8 (Extract w32 0 (SExt w64 N8))
+ const_arr8))))
+ (Eq 7 (Read w8 0 U0))
+ (Eq 13 (Read w8 1 U0))]
+ false []
+ [n_args
+ n_args_1
+ arg0
+ arg1
+ A-data
+ A-data-stat
+ stdin
+ stdin-stat
+ stdout
+ stdout-stat
+ model_version])
+
+array A-data[8] : w32 -> w8 = symbolic
+array A-data-stat[144] : w32 -> w8 = symbolic
+array arg0[11] : w32 -> w8 = symbolic
+array arg1[3] : w32 -> w8 = symbolic
+array model_version[4] : w32 -> w8 = symbolic
+array n_args[4] : w32 -> w8 = symbolic
+array n_args_1[4] : w32 -> w8 = symbolic
+array stdin[8] : w32 -> w8 = symbolic
+array stdin-stat[144] : w32 -> w8 = symbolic
+array stdout[1024] : w32 -> w8 = symbolic
+array stdout-stat[144] : w32 -> w8 = symbolic
+(query [(Ult N0:(ReadLSB w32 0 n_args)
+ 2)
+ (Slt 0 N0)
+ (Ult N1:(ReadLSB w32 0 n_args_1)
+ 3)
+ (Slt 0 N1)
+ (Eq false (Slt 1 N1))
+ (Eq false
+ (Eq 0
+ (And w64 (ReadLSB w64 8 A-data-stat)
+ 2147483647)))
+ (Ult (ReadLSB w64 56 A-data-stat)
+ 65536)
+ (Eq false
+ (Eq 0
+ (And w64 (ReadLSB w64 8 stdin-stat)
+ 2147483647)))
+ (Ult (ReadLSB w64 56 stdin-stat)
+ 65536)
+ (Eq false
+ (Eq 0
+ (And w64 (ReadLSB w64 8 stdout-stat)
+ 2147483647)))
+ (Ult (ReadLSB w64 56 stdout-stat)
+ 65536)
+ (Eq 1
+ (ReadLSB w32 0 model_version))
+ (Eq 45 (Read w8 0 arg0))
+ (Eq 45 (Read w8 1 arg0))
+ (Eq 61 (Read w8 3 arg0))
+ (Eq 116 (Read w8 2 arg0))
+ (Eq false
+ (Eq 0 (Read w8 4 arg0)))
+ (Eq false
+ (Eq 0
+ N2:(Read w8 7 U0:[10=0] @ arg0)))
+ (Eq 0 (Read w8 8 U0))
+ (Eq 11 (Read w8 4 U0))
+ (Eq 63 (Read w8 5 U0))
+ (Eq 8 (Read w8 6 U0))
+ (Eq false (Eq 39 N2))
+ (Or (Eq 122 N2)
+ (Or (Eq 121 N2)
+ (Or (Eq 120 N2)
+ (Or (Eq 119 N2)
+ (Or (Eq 118 N2)
+ (Or (Eq 117 N2)
+ (Or (Eq 116 N2)
+ (Or (Eq 115 N2)
+ (Or (Eq 114 N2)
+ (Or (Eq 113 N2)
+ (Or (Eq 112 N2)
+ (Or (Eq 111 N2)
+ (Or (Eq 110 N2)
+ (Or (Eq 109 N2)
+ (Or (Eq 108 N2)
+ (Or (Eq 107 N2)
+ (Or (Eq 106 N2)
+ (Or (Eq 105 N2)
+ (Or (Eq 104 N2)
+ (Or (Eq 103 N2)
+ (Or (Eq 102 N2)
+ (Or (Eq 101 N2)
+ (Or (Eq 100 N2)
+ (Or (Eq 99 N2)
+ (Or (Eq 98 N2)
+ (Or (Eq 97 N2)
+ (Or (Eq 95 N2)
+ (Or (Eq 93 N2)
+ (Or (Eq 90 N2)
+ (Or (Eq 89 N2)
+ (Or (Eq 88 N2)
+ (Or (Eq 87 N2)
+ (Or (Eq 86 N2)
+ (Or (Eq 85 N2)
+ (Or (Eq 84 N2)
+ (Or (Eq 83 N2)
+ (Or (Eq 82 N2)
+ (Or (Eq 81 N2)
+ (Or (Eq 80 N2)
+ (Or (Eq 79 N2)
+ (Or (Eq 78 N2)
+ (Or (Eq 77 N2)
+ (Or (Eq 76 N2)
+ (Or (Eq 75 N2)
+ (Or (Eq 74 N2)
+ (Or (Eq 73 N2)
+ (Or (Eq 72 N2)
+ (Or (Eq 71 N2)
+ (Or (Eq 70 N2)
+ (Or (Eq 69 N2)
+ (Or (Eq 68 N2)
+ (Or (Eq 67 N2)
+ (Or (Eq 66 N2)
+ (Or (Eq 65 N2)
+ (Or (Eq 58 N2)
+ (Or (Eq 57 N2)
+ (Or (Eq 56 N2)
+ (Or (Eq 55 N2)
+ (Or (Eq 54 N2)
+ (Or (Eq 53 N2)
+ (Or (Eq 52 N2)
+ (Or (Eq 51 N2)
+ (Or (Eq 50 N2)
+ (Or (Eq 49 N2)
+ (Or (Eq 48 N2)
+ (Or (Eq 47 N2)
+ (Or (Eq 46 N2)
+ (Or (Eq 45 N2)
+ (Or (Eq 44 N2)
+ (Or (Eq 43 N2) (Eq 37 N2)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))]
+ false []
+ [n_args
+ arg0
+ n_args_1
+ arg1
+ A-data
+ A-data-stat
+ stdin
+ stdin-stat
+ stdout
+ stdout-stat
+ model_version]) \ No newline at end of file
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-23 19:57:23 +0000