Rewording tests

OCamlPro · Oct 2, 2023 · 390b7d4 · 390b7d4
1 parent 37db150
commit 390b7d4
Show file tree

Hide file tree

Showing 7 changed files with 62 additions and 14 deletions.
diff --git a/tests/dune.inc b/tests/dune.inc
diff --git a/.../smtlib/testfile-get-info.dolmen.expected → ...smtlib/testfile-get-info1.dolmen.expected b/.../smtlib/testfile-get-info.dolmen.expected → ...smtlib/testfile-get-info1.dolmen.expected
@@ -1,4 +1,3 @@
-(error "Invalid (get-info :reason-unknown)")
 
 unknown
 unsupported
@@ -10,4 +9,3 @@ unsupported
 (:name "Alt-Ergo")
 (:reason-unknown Incomplete)
 (:version dev)
-unsupported
diff --git a/tests/smtlib/testfile-get-info.dolmen.smt2 → tests/smtlib/testfile-get-info1.dolmen.smt2 b/tests/smtlib/testfile-get-info.dolmen.smt2 → tests/smtlib/testfile-get-info1.dolmen.smt2
@@ -1,17 +1,14 @@
 (set-logic ALL)
 
 (declare-const x Int)
-(declare-const y Int)
 
 (assert (= (* x x) 4))
 
-(get-info :reason-unknown)
 (check-sat)
 (get-info :all-statistics)
 (get-info :assertion-stack-levels)
 (get-info :authors)
 (get-info :error-behavior)
 (get-info :name)
 (get-info :reason-unknown)
-(get-info :version)
-(get-info :foo)
+(get-info :version)
diff --git a/tests/smtlib/testfile-get-info2.err.dolmen.expected b/tests/smtlib/testfile-get-info2.err.dolmen.expected
@@ -0,0 +1 @@
+(error "Invalid (get-info :reason-unknown)")
diff --git a/tests/smtlib/testfile-get-info2.err.dolmen.smt2 b/tests/smtlib/testfile-get-info2.err.dolmen.smt2
@@ -0,0 +1,8 @@
+(set-logic ALL)
+
+(declare-const x Int)
+
+(assert (= (* x x) 4))
+
+(get-info :reason-unknown)
+(check-sat)
diff --git a/tests/smtlib/testfile-get-info3.dolmen.expected b/tests/smtlib/testfile-get-info3.dolmen.expected
@@ -0,0 +1 @@
+unsupported
diff --git a/tests/smtlib/testfile-get-info3.dolmen.smt2 b/tests/smtlib/testfile-get-info3.dolmen.smt2
@@ -0,0 +1 @@
+(get-info :foo)