mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-10 21:20:52 +00:00
Code Activity

disable assertion for now

Browse source
This commit is contained in:
Jakob Rath 2022-01-20 17:48:19 +01:00
parent daf23cfe02
commit aea3545fcc
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/polysat/explain.cpp
View file

@ -77,7 +77,7 @@ namespace polysat {
premises.push_back(c1); premises.push_back(c1);
premises.push_back(c2); premises.push_back(c2);
core.replace(c2, c, premises); core.replace(c2, c, premises);
SASSERT(l_true == c.bvalue(s)); // SASSERT_EQ(l_true, c.bvalue(s)); // TODO: currently violated, check this!
SASSERT(c.is_currently_false(s)); SASSERT(c.is_currently_false(s));
break; break;
default: default: