Description
For the following program, I am getting different results from different solvers. Bug is unreachable in the program however some of the solvers states it as reachable.
#include <stdio.h>
#include <stdlib.h>
#include <assert.h>
#define loop for(;;)
#define ipoint(var) { int var=nondet_int(); if (var) goto END; }
main() {
int x=0;
int choice =nondet_int();
if (choice) {
x=x+1;
}
else {
x=x+2;
}
if (x==5) __CPROVER_assert(0,"Bug at this point");
}
Output for cbmc undCBMCSmall.c --z3 OR cbmc undCBMCSmall.c --cvc3 OR cbmc undCBMCSmall.c --smt2 is as follows:
CBMC version 5.80.0 (cbmc-5.80.0) 64-bit x86_64 linux
Parsing undCBMCSmall.c
Converting
Type-checking undCBMCSmall
file undCBMCSmall.c line 13 function main: function 'nondet_int' is not declared
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.000688196s
size of program expression: 36 steps
simple slicing removed 6 assignments
Generated 1 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 1.1761e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.000164315s
Running propositional reduction
Post-processing
Runtime Post-process: 3.815e-06s
Solving with MiniSAT 2.2.1 with simplifier
164 variables, 133 clauses
SAT checker inconsistent: instance is UNSATISFIABLE
Runtime Solver: 2.3411e-05s
Runtime decision procedure: 0.000216109s
** Results:
undCBMCSmall.c function main
[main.assertion.1] line 20 Bug at this point: SUCCESS
** 0 of 1 failed (1 iterations)
VERIFICATION SUCCESSFUL
Where for cbmc undCBMCSmall.c --cvc4 OR cbmc undCBMCSmall.c --cvc5 OR cbmc undCBMCSmall.c --yices OR cbmc undCBMCSmall.c --cprover-smt2 OR cbmc undCBMCSmall.c --boolector OR cbmc undCBMCSmall.c --cprover-bitwuzla OR cbmc undCBMCSmall.c --cprover-mathsat is as follows:
CBMC version 5.80.0 (cbmc-5.80.0) 64-bit x86_64 linux
Parsing undCBMCSmall.c
Converting
Type-checking undCBMCSmall
file undCBMCSmall.c line 13 function main: function 'nondet_int' is not declared
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.000728194s
size of program expression: 36 steps
simple slicing removed 6 assignments
Generated 1 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 1.4794e-05s
Passing problem to SMT2 ALL using CVC4
converting SSA
Runtime Convert SSA: 0.000153958s
Running SMT2 ALL using CVC4
Runtime Solver: 0.00277197s
Runtime decision procedure: 0.00298569s
** Results:
undCBMCSmall.c function main
[main.assertion.1] line 20 Bug at this point: ERROR
** 0 of 1 failed (1 iterations)
VERIFICATION ERROR
CBMC version: 5.80.0 (cbmc-5.80.0)
Operating system: Ubuntu 16.04 / macOS Sonoma Version 14.3
Exact command line resulting in the issue: cbmc programname.c --cvc5/ --cvc3/ --cvc4 / .. other SMT solvers
What behaviour did you expect: expecting same behavior from all SMT solvers as "VERIFICATION SUCCESSFUL" since the bug is unreachable
What happened instead: Different solvers gives different results