Add more smt2 tests

formalsec · Sep 13, 2024 · 7fae2c9 · 7fae2c9
1 parent 8404516
commit 7fae2c9
Show file tree

Hide file tree

Showing 6 changed files with 22 additions and 6 deletions.
diff --git a/test/smt2/dune b/test/smt2/dune
@@ -2,7 +2,9 @@
  (enabled_if %{lib-available:z3})
  (deps
   %{bin:smtml}
-  test_bitv_simple.smt2
+  test_bitv_const.smt2
+  test_bitv_sort.smt2
+  test_bitv_funs.smt2
   test_core_all.smt2
   test_core_binary.smt2
   test_core_const.smt2

diff --git a/test/smt2/test_bitv_const.smt2 b/test/smt2/test_bitv_const.smt2
@@ -0,0 +1,3 @@
+(declare-fun symbol_0 () (_ BitVec 32))
+(assert (= symbol_0 (_ bv0 32)))
+(check-sat)
diff --git a/test/smt2/test_bitv_funs.smt2 b/test/smt2/test_bitv_funs.smt2
@@ -0,0 +1,9 @@
+(declare-const x (_ BitVec 32))
+(declare-const y (_ BitVec 32))
+(declare-const z (_ BitVec 32))
+(declare-const u (_ BitVec 65))
+(declare-const v (_ BitVec 64))
+(declare-const w (_ BitVec 64))
+(assert (= x (bvnot (bvnot x))))
+(assert (= (bvneg y) (bvneg y)))
+(check-sat)
diff --git a/test/smt2/test_bitv_simple.smt2 b/test/smt2/test_bitv_simple.smt2
diff --git a/test/smt2/test_bitv_sort.smt2 b/test/smt2/test_bitv_sort.smt2
@@ -0,0 +1,3 @@
+(declare-fun symbol_0 () (_ BitVec 8))
+(declare-fun symbol_1 () (_ BitVec 32))
+(declare-fun symbol_2 () (_ BitVec 64))
diff --git a/test/smt2/test_smt2.t b/test/smt2/test_smt2.t
@@ -43,5 +43,8 @@ Test String parsing:
     (x "abcd"))
 
 Test BitVector parsing:
-  $ smtml run test_bitv_simple.smt2
+  $ smtml run test_bitv_sort.smt2
+  $ smtml run test_bitv_const.smt2
+  sat
+  $ smtml run test_bitv_funs.smt2
   sat