Inconsistency in the results by different SMT solvers

[ArpitaDutta]

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

[martin-cs]

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.

[kroening]

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.

[tautschnig]

I believe #8378 will also address this one.