From c4b4ffb4bf5577fd26a95e5ae430e2250f3211df Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Thu, 23 Nov 2023 12:13:51 +0100 Subject: [PATCH] Poetry --- tests/smtlib/testfile-steps-bound.dolmen.smt2 | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/tests/smtlib/testfile-steps-bound.dolmen.smt2 b/tests/smtlib/testfile-steps-bound.dolmen.smt2 index be770cecfc..ed9711b987 100644 --- a/tests/smtlib/testfile-steps-bound.dolmen.smt2 +++ b/tests/smtlib/testfile-steps-bound.dolmen.smt2 @@ -4,19 +4,23 @@ (declare-const y Int) (assert (= (* x x) 3)) -; Should answer 'unknown' (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) -; Should answer 'unsat' (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