mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-22 08:17:37 +00:00
Code Activity

keep literals alive

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2026-02-18 07:23:22 -10:00
parent 138828259a
commit b60e0e0dd3
1 changed files with 5 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/test/nlsat.cpp
View file

@ -2562,9 +2562,11 @@ static void tst_explain_p6236() {
// jst lit[0]: !(x15 < root[1](p1)) => literal(root_lt_bvar, true) // jst lit[0]: !(x15 < root[1](p1)) => literal(root_lt_bvar, true)
// jst lit[1]: !(p2 > 0) => literal(gt_bvar, true) // jst lit[1]: !(p2 > 0) => literal(gt_bvar, true)
nlsat::bool_var root_lt_bvar = s.mk_root_atom(nlsat::atom::ROOT_LT, x15, 1, p1.get()); nlsat::bool_var root_lt_bvar = s.mk_root_atom(nlsat::atom::ROOT_LT, x15, 1, p1.get());
s.inc_ref(root_lt_bvar);
nlsat::literal jst_lit0(root_lt_bvar, true); // negated: !(x15 < root[1](p1)) nlsat::literal jst_lit0(root_lt_bvar, true); // negated: !(x15 < root[1](p1))
nlsat::literal gt_lit = mk_gt(s, p2.get()); nlsat::literal gt_lit = mk_gt(s, p2.get());
s.inc_ref(gt_lit);
nlsat::literal jst_lit1 = ~gt_lit; // negated: !(p2 > 0) nlsat::literal jst_lit1 = ~gt_lit; // negated: !(p2 > 0)
nlsat::literal jst_lits[2] = { jst_lit0, jst_lit1 }; nlsat::literal jst_lits[2] = { jst_lit0, jst_lit1 };
@ -2642,6 +2644,9 @@ static void tst_explain_p6236() {
} }
ENSURE(unsat); ENSURE(unsat);
s.dec_ref(root_lt_bvar);
s.dec_ref(gt_lit);
std::cout << "=== END tst_explain_p6236 ===\n\n"; std::cout << "=== END tst_explain_p6236 ===\n\n";
} }