Exception when processing SAT assignment with cryptominisat

[zhassan-aws]

I'm trying to use https://github.com/msoos/cryptominisat as an external SAT solver. It seems to cause an issue if the test has a counterexample, e.g.

$ cat fail.c 
#include "assert.h"

int main() {
  int x;
  int y = x;
  assert(y != x);

  return 0;
}
$ which cryptominisat5
/home/ubuntu/git/cryptominisat/build/cryptominisat5
$ cbmc fail.c --external-sat-solver cryptominisat5
CBMC version 5.66.0 (cbmc-5.66.0) 64-bit x86_64 linux
Parsing fail.c
Converting
Type-checking fail
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.000673871s
size of program expression: 39 steps
simple slicing removed 5 assignments
Generated 1 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 9.28e-06s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 7.9941e-05s
Running propositional reduction
Post-processing
Runtime Post-process: 1.646e-05s
Solving with External SAT solver
Writing temporary CNF
Invoking SAT solver
Solver returned code: 10
result:SATISFIABLE
SAT assignment  caused an exception while processing
Runtime Solver: 0.00365672s
Runtime decision procedure: 0.00378501s

** Results:
fail.c function main
[main.assertion.1] line 6 assertion y != x: ERROR

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

If I change the assert to

assert(y == x)

verification succeeds:

$ cbmc fail.c --external-sat-solver cryptominisat5
CBMC version 5.66.0 (cbmc-5.66.0) 64-bit x86_64 linux
Parsing fail.c
Converting
Type-checking fail
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.000568689s
size of program expression: 39 steps
simple slicing removed 5 assignments
Generated 1 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 9.23e-06s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 8.4671e-05s
Running propositional reduction
Post-processing
Runtime Post-process: 2.2421e-05s
Solving with External SAT solver
Writing temporary CNF
Invoking SAT solver
Solver returned code: 20
result:UNSATISFIABLE
Runtime Solver: 0.003168s
Runtime decision procedure: 0.00330383s

** Results:
fail.c function main
[main.assertion.1] line 6 assertion y == x: SUCCESS

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

Does cryptominisat not produce the correct output that CBMC needs in case of a satisfiable instance?

CBMC version: 5.66.0
Operating system: Ubuntu 20.04
Exact command line resulting in the issue:
What behaviour did you expect:
What happened instead:

[feliperodri]

@diffblue/diffblue-opensource