CBMC crashes or produces wrong result when using external SAT solvers

[aaronbembenek-aws]

This is following up on model-checking/kani#1962.

CBMC version: 5.71.0
cryptominisat version: 5.11.4
kissat version: 3.0.0
Operating system: macOS Monterey
Exact command line resulting in the issue:

cbmc --bounds-check --pointer-check --div-by-zero-check --float-overflow-check --nan-check --undefined-shift-check --unwinding-assertions --object-bits 16 --slice-formula lib.for-failing_harness.out --json-ui
cbmc --bounds-check --pointer-check --div-by-zero-check --float-overflow-check --nan-check --undefined-shift-check --unwinding-assertions --object-bits 16 --slice-formula lib.for-failing_harness.out --json-ui --external-sat-solver cryptominisat5
cbmc --bounds-check --pointer-check --div-by-zero-check --float-overflow-check --nan-check --undefined-shift-check --unwinding-assertions --object-bits 16 --slice-formula lib.for-failing_harness.out --json-ui --external-sat-solver kissat

What behaviour did you expect:

I expected to get the same verification results whether running with an external SAT solver or not.

What happened instead:

When not using an external SAT solver, CBMC reports that 4 properties fail.

When using cryptominisat as an external SAT solver, CBMC crashes with an invariant violation:

  }--- begin invariant violation report ---
Invariant check failed
File: /tmp/cbmc-20221124-3566-1xvskin/src/goto-checker/goto_trace_storage.cpp:29 function: insert
Condition: emplace_result.second
Reason: cannot associate more than one error trace with property __rust_dealloc.precondition_instance.1
Backtrace:
0   cbmc                                0x0000000103154b18 _Z15print_backtraceRNSt3__113basic_ostreamIcNS_11char_traitsIcEEEE + 120
1   cbmc                                0x0000000103154ed0 _Z13get_backtracev + 44
2   cbmc                                0x0000000102cde728 _Z29invariant_violated_structuredI17invariant_failedtJRKNSt3__112basic_stringIcNS1_11char_traitsIcEENS1_9allocatorIcEEEEEENS1_9enable_ifIXsr3std10is_base_ofIS0_T_EE5valueEvE4typeES9_S9_iS9_DpOT0_ + 52
3   cbmc                                0x0000000102cde658 _ZNSt3__112basic_stringIcNS_11char_traitsIcEENS_9allocatorIcEEEC1IDnEEPKc + 0
4   cbmc                                0x0000000102cf674c _ZN19goto_trace_storaget6insertEO11goto_tracet + 392
5   cbmc                                0x0000000102ced988 _ZN43all_properties_verifier_with_trace_storagetI25multi_path_symex_checkertEclEv + 228
6   cbmc                                0x0000000102ce5d80 _ZN19cbmc_parse_optionst4doitEv + 2788
7   cbmc                                0x000000010317f088 _ZN19parse_options_baset4mainEv + 180
8   cbmc                                0x0000000102cde008 main + 48
9   dyld                                0x00000001038b508c start + 520


--- end invariant violation report ---

When using kissat as an external SAT solver, CBMC reports that 17 properties fail. For example, the property std::alloc::Layout::align.pointer_dereference.4 succeeds with the internal solver but fails with kissat.

I've attached the relevant Goto binary. Thanks!

lib.for-failing_harness.out.tar.gz

[zhassan-aws]

Somewhat similar behavior can be seen on this C 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;
}

where running it with the default solver results in 1 failure,:

$ cbmc test.c
...
** 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 running it with an external sat solver (kissat, cadical, or cryptominsat) results in 2 failures:

$ cbmc test.c --external-sat-solver kissat
...
** 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

[zhassan-aws]

Yet another small reproducer:

#include <assert.h>

int main() {
    int x;
    if (x >= 0) {
        assert(0);
    } else {
        assert(x < 0);
    }
    return 0;
}

$ cbmc branch.c 
CBMC version 5.72.0 (cbmc-5.72.0) 64-bit x86_64 linux
Parsing branch.c
...
** Results:
branch.c function main
[main.assertion.1] line 6 assertion 0: FAILURE
[main.assertion.2] line 8 assertion x < 0: SUCCESS

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

$ cbmc branch.c --external-sat-solver kissat
CBMC version 5.72.0 (cbmc-5.72.0) 64-bit x86_64 linux
Parsing branch.c
...
** Results:
branch.c function main
[main.assertion.1] line 6 assertion 0: FAILURE
[main.assertion.2] line 8 assertion x < 0: FAILURE

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