Skip to content

Commit 778962e

Browse files
committed
Add test of the setup commands sent to smt2 solver
1 parent 3e9b4a8 commit 778962e

File tree

1 file changed

+3
-1
lines changed

1 file changed

+3
-1
lines changed

regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,9 @@
11
CORE
22
test.c
3-
--incremental-smt2-solver "z3 --smt2 -in"
3+
--incremental-smt2-solver "z3 --smt2 -in" --verbosity 10
44
Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
5+
Sending command to SMT2 solver - \(set-option :produce-models true\)
6+
Sending command to SMT2 solver - \(set-logic QF_UFBV\)
57
^EXIT=(0|127|134|137)$
68
^SIGNAL=0$
79
identifier: main::1::x

0 commit comments

Comments
 (0)