Incorrect result for --external-sat-solver z3 option

[ArpitaDutta]

CBMC version: 5.80.0 (cbmc-5.80.0) Operating system:Ubuntu 16.04 Exact command line resulting in the issue: cbmc undCBMCSmall.c --external-sat-solver z3 What behaviour did you expect: VERIFICATION SUCCESSFUL What happened instead: VERIFICATION ERROR

For the following program, I am getting VERIFICATION ERROR whereas the bug is unreachable in the program.

#include <stdio.h>
#include <stdlib.h>
#include <assert.h>

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 obtained:

$ cbmc undCBMCSmall.c --external-sat-solver z3
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 9 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.00070634s
size of program expression: 36 steps
simple slicing removed 6 assignments
Generated 1 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 1.4386e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.000109918s
Running propositional reduction
Post-processing
Runtime Post-process: 3.689e-06s
Solving with External SAT solver
Writing temporary CNF
Invoking SAT solver
Solver returned code: 0
external SAT solver has provided an unexpected response
Runtime Solver: 0.00331865s
Runtime decision procedure: 0.00347998s

** Results:
undCBMCSmall.c function main
[main.assertion.1] line 16 Bug at this point: ERROR

** 0 of 1 failed (1 iterations)
VERIFICATION ERROR

[martin-cs]

If you want to use z3, I would suggest using it via the SMT interface. I think z3 has a DIMACS interface but it's a bit of a strange way to use it.

[remi-delmas-3000]

Try using

cbmc --incremental-smt2-solver 'z3 --smt2 -in'  yourfile.c

or

cbmc --smt2  yourfile.c