mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-23 03:27:52 +00:00
Code Activity

fix assertion violation in the code path where the simplifier throws a memout exception

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-14 16:37:53 -08:00
parent 31d4ba0009
commit 076d3dbf13
3 changed files with 6 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/sat/sat_integrity_checker.cpp
View file

@ -45,6 +45,7 @@ namespace sat {
}
bool integrity_checker::check_clause(clause const & c) const {
CTRACE("sat_bug", c.was_removed(), s.display(tout << "c: " << c.id() << ": " << c << "\n"));
SASSERT(!c.was_removed());
for (unsigned i = 0; i < c.size(); i++) {
VERIFY(c[i].var() <= s.num_vars());