Issues
- 3
- 0
Make C++ support more visible
#8272 opened by intrigus-lgtm - 1
CodeQL reports potential double free in XML parser
#8262 opened by tautschnig - 1
JBMC does not support AtomicBoolean.
#8263 opened by ben-Draeger - 1
What are the semantics of (repeated) declaration and DEAD for a single symbol?
#8258 opened by tautschnig - 2
- 0
goto-analyzer fails with an irep.data nullptr
#8256 opened by rurban - 0
Invariant violation in `local_bitvector_analysist` when `--export-file-local-symbols` is used
#8254 opened by remi-delmas-3000 - 1
Custom ipasir SAT implementation: "libcprover-cpp cannot be linked as dependency" error
#8249 opened by Geremia - 0
Usage of string format specifier in `__CPROVER_printf`?
#8204 opened by gleachkr - 1
Conversion error with _Generic + array
#8243 opened by P-p-H-d - 0
goto-gcc -D_FORTIFY_SOURCE=3 : /usr/include/bits/stdio2.h:31:1: warning: function '__builtin_dynamic_object_size' is not declared
#8116 opened by vt-alt - 4
Test failures with GCC 14
#8163 opened by lzaoral - 0
Memory blowup during typechecking
#8228 opened by remi-delmas-3000 - 0
`--nondet-static-exclude` silently fails
#8225 opened by feliperodri - 1
Semantics of assert statements
#8223 opened by salvadorer - 9
- 2
- 1
Unexpected failure with array_copy/array_equals
#8176 opened by remi-delmas-3000 - 0
- 2
SMT solving is not invoked with `--incremental-loop`
#8185 opened by nianzelee - 5
CBMC reporting incosistently assertion failures
#8196 opened by salvadorer - 12
Puzzling strcmp behavior
#8173 opened by gleachkr - 1
- 2
cbmc --show-properties fails
#8165 opened by nmanthey - 1
Xen integration test compilation fails
#8193 opened by polgreen - 4
Build with system CaDiCaL
#8113 opened by kotopesutility - 4
- 2
Negative Boolean variables in CNF's comments
#8172 opened by olegzaikin - 0
- 3
Integer to pointer casting behaviour?
#8103 opened by ShaleXIONG - 1
Inconsistent results from pointer comparison
#8161 opened by Anthonysdu - 0
Wrong --conversion-check in cast from double to unsigned
#8131 opened by cesaro - 0
- 1
Unsound optimization of pointer dereferencing
#8128 opened by cesaro - 0
- 0
Bugs in multiple interval_template.h methods
#8144 opened by cesaro - 2
CBMC's pointer check results maybe conflicting?
#8111 opened by M-ouse - 1
`byte_extract` is not appearing on the rhs of trace assignment when using the incremental smt2 decision procedure
#8076 opened by esteffin - 0
Multidimensional arrays?
#8096 opened by DennisYurichev - 0
Old version of Z3 causes extremely slow solving times in incremental smt2 decision procedure
#8083 opened by esteffin - 0
Support for inlined `struct` type is not yet implemented in incremental smt2 decision procedure
#8078 opened by esteffin - 0
- 0
Broken support for `address_of(labelt)` in incremental smt2 decision procedure.
#8079 opened by esteffin - 0
`array_exprt` is not handled correctly in the incremental smt2 decision procedure
#8080 opened by esteffin - 0
Support for `empty` types is not yet implemented in incremental smt2 decision procedure
#8077 opened by esteffin - 0
Support for typecasting between 2 types of arrays is not yet implemented in incremental smt2 decision procedure
#8075 opened by esteffin - 0
Support for arithmetic Integers is not yet implemented in incremental smt2 decision procedure
#8074 opened by esteffin - 0
Support for the internal push/pop interface is unimplemented in incremental smt2 decision procedure
#8073 opened by thomasspriggs - 0
For some tests duplicate and/or missing declarations involving arrays cause problems in incremental smt2 decision procedure
#8072 opened by thomasspriggs