You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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
The text was updated successfully, but these errors were encountered:
Please forgive me if this question is patronising or stupid but ... do you have all of these solvers installed and on the command-line path? CBMC does not build them in, you have to install them separately.
Please forgive me if this question is patronising or stupid but ... do you have all of these solvers installed and on the command-line path? CBMC does not build them in, you have to install them separately.
We should add a "solver executable not found, please install" message.
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.
Output for
cbmc undCBMCSmall.c --z3
ORcbmc undCBMCSmall.c --cvc3
ORcbmc undCBMCSmall.c --smt2
is as follows:Where for
cbmc undCBMCSmall.c --cvc4
ORcbmc undCBMCSmall.c --cvc5
ORcbmc undCBMCSmall.c --yices
ORcbmc undCBMCSmall.c --cprover-smt2
ORcbmc undCBMCSmall.c --boolector
ORcbmc undCBMCSmall.c --cprover-bitwuzla
ORcbmc undCBMCSmall.c --cprover-mathsat
is as follows: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
The text was updated successfully, but these errors were encountered: