diff --git a/src/lib/frontend/d_state_option.ml b/src/lib/frontend/d_state_option.ml index 20014abdf7..3c5d807c7d 100644 --- 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 index fbfb009573..d655d635b8 100644 --- a/tests/dune.inc +++ b/tests/dune.inc @@ -204314,8 +204314,8 @@ ; Auto-generated part begin (subdir smtlib (rule - (target testfile-steps-bound.dolmen_dolmen.output) - (deps (:input testfile-steps-bound.dolmen.smt2)) + (target testfile-steps-bound2.dolmen_dolmen.output) + (deps (:input testfile-steps-bound2.dolmen.smt2)) (package alt-ergo) (action (chdir %{workspace_root} @@ -204329,11 +204329,32 @@ --frontend dolmen %{input}))))))) (rule - (deps testfile-steps-bound.dolmen_dolmen.output) + (deps testfile-steps-bound2.dolmen_dolmen.output) (alias runtest-quick) (package alt-ergo) (action - (diff testfile-steps-bound.dolmen.expected testfile-steps-bound.dolmen_dolmen.output))) + (diff testfile-steps-bound2.dolmen.expected testfile-steps-bound2.dolmen_dolmen.output))) + (rule + (target testfile-steps-bound1.dolmen.err_dolmen.output) + (deps (:input testfile-steps-bound1.dolmen.err.smt2)) + (package alt-ergo) + (action + (chdir %{workspace_root} + (with-stdout-to %{target} + (ignore-stderr + (with-accepted-exit-codes (or 1) + (run %{bin:alt-ergo} + --timelimit=2 + --enable-assertions + --output=smtlib2 + --frontend dolmen + %{input}))))))) + (rule + (deps testfile-steps-bound1.dolmen.err_dolmen.output) + (alias runtest-quick) + (package alt-ergo) + (action + (diff testfile-steps-bound1.dolmen.err.expected testfile-steps-bound1.dolmen.err_dolmen.output))) (rule (target testfile-reset_ci_cdcl_no_minimal_bj.output) (deps (:input testfile-reset.smt2)) diff --git a/tests/smtlib/testfile-steps-bound.dolmen.smt2 b/tests/smtlib/testfile-steps-bound.dolmen.smt2 deleted file mode 100644 index ed9711b987..0000000000 --- a/tests/smtlib/testfile-steps-bound.dolmen.smt2 +++ /dev/null @@ -1,26 +0,0 @@ -(set-logic ALL) - -(declare-const x Int) -(declare-const y Int) -(assert (= (* x x) 3)) - -(push 1) -; Setting this option here should fail because the previous assertion takes -; more than 2 steps. It does not because AE does not execute SMTLIB instruction -; imperatively; here, the option is actually set before the assertion is -; executed. -(set-option :steps-bound 2) -; Should answer 'unknown' -(check-sat) -(get-info :reason-unknown) -(pop 1) - -(reset) - -(set-logic ALL) -(declare-const x Int) -(declare-const y Int) -(set-option :steps-bound 100) -; Should answer 'unsat' -(assert (= (* x x) 3)) -(check-sat) \ No newline at end of file diff --git a/tests/smtlib/testfile-steps-bound1.dolmen.err.expected b/tests/smtlib/testfile-steps-bound1.dolmen.err.expected new file mode 100644 index 0000000000..90f9e3c816 --- /dev/null +++ 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 new file mode 100644 index 0000000000..2da3ac5d7f --- /dev/null +++ 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) \ No newline at end of file diff --git a/tests/smtlib/testfile-steps-bound.dolmen.expected b/tests/smtlib/testfile-steps-bound2.dolmen.expected similarity index 100% rename from tests/smtlib/testfile-steps-bound.dolmen.expected rename to tests/smtlib/testfile-steps-bound2.dolmen.expected diff --git a/tests/smtlib/testfile-steps-bound2.dolmen.smt2 b/tests/smtlib/testfile-steps-bound2.dolmen.smt2 new file mode 100644 index 0000000000..3d578cf450 --- /dev/null +++ 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) \ No newline at end of file