Adding tests

OCamlPro · Nov 6, 2023 · 9cbf833 · 9cbf833
1 parent 86f8f33
commit 9cbf833
Show file tree

Hide file tree

Showing 5 changed files with 60 additions and 0 deletions.
diff --git a/tests/dune.inc b/tests/dune.inc
diff --git a/tests/smtlib/testfile-get-assignment1.err.dolmen.expected b/tests/smtlib/testfile-get-assignment1.err.dolmen.expected
@@ -0,0 +1 @@
+(error "No model produced, cannot execute get-assignment.")
diff --git a/tests/smtlib/testfile-get-assignment1.err.dolmen.smt2 b/tests/smtlib/testfile-get-assignment1.err.dolmen.smt2
@@ -0,0 +1,3 @@
+(set-logic ALL)
+; The next instruction should fail because we did not generate a model
+(get-assignment)
diff --git a/tests/smtlib/testfile-get-assignment2.err.dolmen.expected b/tests/smtlib/testfile-get-assignment2.err.dolmen.expected
@@ -0,0 +1,6 @@
+
+unknown
+(
+  (define-fun x () Int 0)
+)
+(error "Produce assignments disabled; add (set-option :produce-assignments true)")
diff --git a/tests/smtlib/testfile-get-assignment2.err.dolmen.smt2 b/tests/smtlib/testfile-get-assignment2.err.dolmen.smt2
@@ -0,0 +1,8 @@
+(set-logic ALL)
+(set-option :produce-models true)
+(declare-const x Int)
+(assert (! (= x 0) :named foo))
+(check-sat)
+(get-model)
+; The next instruction should fail because we did not activate the option
+(get-assignment)
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		(error "No model produced, cannot execute get-assignment.")