Update tests

Stevendeo · Nov 27, 2023 · d14ddf7 · d14ddf7
1 parent 3ae190b
commit d14ddf7
Show file tree

Hide file tree

Showing 7 changed files with 51 additions and 31 deletions.
diff --git a/src/lib/frontend/d_state_option.ml b/src/lib/frontend/d_state_option.ml
@@ -128,7 +128,7 @@ module SatSolver = (val msatsolver)
 
 let msteps =
   let on_update _ sat st = Steps.set_steps_bound sat; st in
-  (create_opt ~on_update "steps_bound" O.get_steps_bound)
+  (create_opt_only_start_mode ~on_update "steps_bound" O.get_steps_bound)
 
 module Steps = (val msteps)
 

diff --git a/tests/dune.inc b/tests/dune.inc
diff --git a/tests/smtlib/testfile-steps-bound.dolmen.smt2 b/tests/smtlib/testfile-steps-bound.dolmen.smt2
diff --git a/tests/smtlib/testfile-steps-bound1.dolmen.err.expected b/tests/smtlib/testfile-steps-bound1.dolmen.err.expected
@@ -0,0 +1 @@
+(error "Invalid action during mode Util.Assert: Set option steps_bound")
diff --git a/tests/smtlib/testfile-steps-bound1.dolmen.err.smt2 b/tests/smtlib/testfile-steps-bound1.dolmen.err.smt2
@@ -0,0 +1,7 @@
+(set-logic ALL)
+
+(declare-const x Int)
+(assert (= (* x x) 3))
+(set-option :steps-bound 2)
+; Should fail because this option cannot be set after set-logic
+(check-sat)
diff --git a/...tlib/testfile-steps-bound.dolmen.expected → ...lib/testfile-steps-bound2.dolmen.expected b/...tlib/testfile-steps-bound.dolmen.expected → ...lib/testfile-steps-bound2.dolmen.expected
diff --git a/tests/smtlib/testfile-steps-bound2.dolmen.smt2 b/tests/smtlib/testfile-steps-bound2.dolmen.smt2
@@ -0,0 +1,17 @@
+(set-option :steps-bound 2)
+(set-logic ALL)
+
+(declare-const x Int)
+(assert (= (* x x) 3))
+; Should answer 'unknown'
+(check-sat)
+(get-info :reason-unknown)
+
+(reset)
+
+(set-option :steps-bound 100)
+(set-logic ALL)
+(declare-const x Int)
+(assert (= (* x x) 3))
+; Should answer 'unsat'
+(check-sat)
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		(error "Invalid action during mode Util.Assert: Set option steps_bound")