diff options
Diffstat (limited to 'test/Solver')
| -rw-r--r-- | test/Solver/FastCexSolver.pc | 12 | ||||
| -rw-r--r-- | test/Solver/dg.exp | 3 |
2 files changed, 15 insertions, 0 deletions
diff --git a/test/Solver/FastCexSolver.pc b/test/Solver/FastCexSolver.pc new file mode 100644 index 00000000..10cdce48 --- /dev/null +++ b/test/Solver/FastCexSolver.pc @@ -0,0 +1,12 @@ +# RUN: %kleaver --use-fast-cex-solver --use-dummy-solver %s > %t +# RUN: not grep FAIL %t + +array arr1[4] : w32 -> w8 = symbolic +(query [] (Not (Eq 4096 (ReadLSB w32 0 arr1)))) + +array arr2[2] : w32 -> w8 = symbolic +(query [(Ule (Add w8 208 N0:(Read w8 0 arr2)) + 9)] + (Eq 52 N0)) + + diff --git a/test/Solver/dg.exp b/test/Solver/dg.exp new file mode 100644 index 00000000..94fc4df8 --- /dev/null +++ b/test/Solver/dg.exp @@ -0,0 +1,3 @@ +load_lib llvm.exp + +RunLLVMTests [lsort [glob -nocomplain $srcdir/$subdir/*.{pc}]] |