We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 332e14d commit 52d5788Copy full SHA for 52d5788
regression/cbmc-incr-smt2/bitvector-arithmetic-operators/simple_equation.desc
@@ -1,6 +1,6 @@
1
CORE
2
simple_equation.c
3
---incremental-smt2-solver 'z3 --smt2 -in' --trace
+--incremental-smt2-solver 'z3 --smt2 -in' --trace --verbosity 10
4
\[main\.assertion\.1\] line \d+ a plus a always equals two times a: SUCCESS
5
\[main\.assertion\.2\] line \d+ a minus a always equals 0: SUCCESS
6
\[main\.assertion\.3\] line \d+ a plus its additive inverse equals 0: SUCCESS
0 commit comments