Promote tests

formalsec · Dec 2, 2024 · 4e85919 · 4e85919
1 parent 23f9a8c
commit 4e85919
Show file tree

Hide file tree

Showing 4 changed files with 42 additions and 42 deletions.
diff --git a/test/smt2/test_smt2.t b/test/smt2/test_smt2.t
@@ -19,10 +19,10 @@ Test Bool parsing:
   sat
   sat
   (model
-    (w false)
-    (x true)
-    (y true)
-    (z true))
+    (w bool false)
+    (x bool true)
+    (y bool true)
+    (z bool true))
 
 Test Int parsing:
   $ smtml run test_lia.smt2
@@ -33,15 +33,15 @@ Test Real parsing:
   $ smtml run test_lra.smt2
   sat
   (model
-    (x 2.)
-    (y 4.))
+    (x real 2.)
+    (y real 4.))
 
 Test String parsing:
   $ smtml run test_string_all.smt2
   sat
   (model
-    (x "abcd")
-    (y "a"))
+    (x str "abcd")
+    (y str "a"))
 
 Test BitVector parsing:
   $ smtml run test_bitv_sort.smt2
@@ -67,18 +67,18 @@ Tests smt2 with the --from-file argument:
   sat
   sat
   (model
-    (w false)
-    (x true)
-    (y true)
-    (z true))
+    (w bool false)
+    (x bool true)
+    (y bool true)
+    (z bool true))
   sat
   sat
   sat
   (model
-    (x -2.)
-    (y 4.))
+    (x real -2.)
+    (y real 4.))
   sat
   sat
   (model
-    (x "abcd")
-    (y "a"))
+    (x str "abcd")
+    (y str "a"))
diff --git a/test/smtml/test_smtml.t b/test/smtml/test_smtml.t
@@ -3,10 +3,10 @@ Test boolean parsing:
   sat
   sat
   (model
-    (w false)
-    (x true)
-    (y true)
-    (z true))
+    (w bool false)
+    (x bool true)
+    (y bool true)
+    (z bool true))
 
  Test int parsing:
   $ smtml run test_lia.smtml
@@ -17,35 +17,35 @@ Test boolean parsing:
   $ smtml run test_lra.smtml
   sat
   (model
-    (x 2.)
-    (y 4.))
+    (x real 2.)
+    (y real 4.))
 
  Test fp parsing:
   $ smtml run test_qf_fp.smtml
   unsat
   sat
   sat
   (model
-    (v (f32 -0.))
-    (w (f32 -0.))
-    (x (f32 0.504000008106))
-    (z (f32 1.)))
+    (v f32 -0.)
+    (w f32 -0.)
+    (x f32 0.504000008106)
+    (z f32 1.))
   sat
   (model
-    (v (f32 -2.))
-    (w (f32 -3.))
-    (x (f32 -2.70000004768))
-    (z (f32 -2.)))
+    (v f32 -2.)
+    (w f32 -3.)
+    (x f32 -2.70000004768)
+    (z f32 -2.))
   sat
   sat
   (model
-    (r (f64 infinity))
-    (s (f64 -3.38460706455e+125))
-    (y (f64 314159265359.)))
+    (r f64 infinity)
+    (s f64 -3.38460706455e+125)
+    (y f64 314159265359.))
 
  Test parsing string:
   $ smtml run test_qf_s.smtml
   sat
   (model
-    (x "abcd"))
+    (x str "abcd"))
 
diff --git a/test/solver/test_altergo.expected b/test/solver/test_altergo.expected
@@ -1,5 +1,5 @@
 (model
-  (w (i32 4))
-  (x (i32 1))
-  (y (i32 2))
-  (z (i32 3)))
+  (w i32 4)
+  (x i32 1)
+  (y i32 2)
+  (z i32 3))
diff --git a/test/solver/test_z3.expected b/test/solver/test_z3.expected
@@ -1,5 +1,5 @@
 (model
-  (w (i32 4))
-  (x (i32 1))
-  (y (i32 2))
-  (z (i32 3)))
+  (w i32 4)
+  (x i32 1)
+  (y i32 2)
+  (z i32 3))