mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 00:55:31 +00:00
Code Activity

assert

Browse source
This commit is contained in:
Jakob Rath 2023-01-18 18:43:41 +01:00
parent 8385452d91
commit 905144cdbb
1 changed files with 11 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/math/polysat/ule_constraint.cpp
View file

@ -184,6 +184,17 @@ namespace polysat {
ule_pp const old_ule(to_lbool(old_is_positive), old_lhs, old_rhs);
ule_pp const new_ule(to_lbool(is_positive), lhs, rhs);
LOG("Simplify: " << old_ule << " --> " << new_ule);
// always-false and always-true constraints should be rewritten to 0 != 0 and 0 == 0, respectively.
if (is_always_false(old_is_positive, old_lhs, old_rhs)) {
SASSERT(!is_positive);
SASSERT(lhs.is_zero());
SASSERT(rhs.is_zero());
}
if (is_always_true(old_is_positive, old_lhs, old_rhs)) {
SASSERT(is_positive);
SASSERT(lhs.is_zero());
SASSERT(rhs.is_zero());
}
}
#endif
}