Incorrect results with an external SAT solver

[zhassan-aws]

On the following program:

#include <assert.h>

int main() {
  int x[1];
  x[0] = 0;
  int y;
  if (y >= 0 && y < 1) {
    assert(0);
    assert(x[y] == y);
  }
  return 0;
}

If I run this with the default SAT solver, I get one failure as expected:

$ cbmc test.c
CBMC version 5.72.0 (cbmc-5.72.0) 64-bit x86_64 linux
Parsing test.c
Converting
Type-checking test
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.000713953s
size of program expression: 42 steps
simple slicing removed 5 assignments
Generated 2 VCC(s), 2 remaining after simplification
Runtime Postprocess Equation: 9.651e-06s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.000365267s
Running propositional reduction
Post-processing
Runtime Post-process: 2.2591e-05s
Solving with MiniSAT 2.2.1 with simplifier
388 variables, 629 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.000265702s
Runtime decision procedure: 0.000671191s
Running propositional reduction
Solving with MiniSAT 2.2.1 with simplifier
388 variables, 0 clauses
SAT checker inconsistent: instance is UNSATISFIABLE
Runtime Solver: 5.92e-06s
Runtime decision procedure: 1.2e-05s

** Results:
test.c function main
[main.assertion.1] line 8 assertion 0: FAILURE
[main.assertion.2] line 9 assertion x[y] == y: SUCCESS

** 1 of 2 failed (2 iterations)
VERIFICATION FAILED

But if I run it with kissat , both assertions fail:

$ cbmc test.c --external-sat-solver kissat
CBMC version 5.72.0 (cbmc-5.72.0) 64-bit x86_64 linux
Parsing test.c
Converting
Type-checking test
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.000781506s
size of program expression: 42 steps
simple slicing removed 5 assignments
Generated 2 VCC(s), 2 remaining after simplification
Runtime Postprocess Equation: 1.9751e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.000206609s
Running propositional reduction
Post-processing
Runtime Post-process: 1.349e-05s
Solving with External SAT solver
Writing temporary CNF
Invoking SAT solver
Solver returned code: 10
result:SATISFIABLE
Runtime Solver: 0.00189018s
Runtime decision procedure: 0.00215949s
Running propositional reduction
Solving with External SAT solver
Writing temporary CNF
Invoking SAT solver
Solver returned code: 10
result:SATISFIABLE
Runtime Solver: 0.00140601s
Runtime decision procedure: 0.00143316s

** Results:
test.c function main
[main.assertion.1] line 8 assertion 0: FAILURE
[main.assertion.2] line 9 assertion x[y] == y: FAILURE

** 2 of 2 failed (3 iterations)
VERIFICATION FAILED

The same thing happens if I run it with cadical or cryptominisat.

CBMC version: 5.72.0
Operating system: Ubuntu 18.04

[zhassan-aws]

Duplicate of #7416. Closing. Will post the C Program there.