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

Disable merging of p<q and p=q in lemmas for now (cf. test_band5)

Browse source
This commit is contained in:
Jakob Rath 2022-12-22 19:25:50 +01:00
parent fa0a481fc8
commit f025d0ad63
1 changed files with 8 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/math/polysat/simplify_clause.cpp
View file

@ -115,6 +115,14 @@ namespace polysat {
continue;
if (c->is_eq())
continue;
#if 1
// Disable the case p<q && p=q for now.
// The merging of less-than and equality may remove premises from the lemma.
// See test_band5.
// TODO: fix and re-enable
if (c.is_negative())
continue;
#endif
LOG_V(10, "Examine: " << lit_pp(s, lit));
pdd const p = c->to_ule().lhs();
pdd const q = c->to_ule().rhs();