From b60e0e0dd33fdd3ce5a655146d8d2e75409ae8a7 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 18 Feb 2026 07:23:22 -1000 Subject: [PATCH] keep literals alive Signed-off-by: Lev Nachmanson --- src/test/nlsat.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/test/nlsat.cpp b/src/test/nlsat.cpp index 6d59a7ff5..1920d569a 100644 --- a/src/test/nlsat.cpp +++ b/src/test/nlsat.cpp @@ -2562,9 +2562,11 @@ static void tst_explain_p6236() { // jst lit[0]: !(x15 < root[1](p1)) => literal(root_lt_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()); + s.inc_ref(root_lt_bvar); nlsat::literal jst_lit0(root_lt_bvar, true); // negated: !(x15 < root[1](p1)) 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_lits[2] = { jst_lit0, jst_lit1 }; @@ -2642,6 +2644,9 @@ static void tst_explain_p6236() { } ENSURE(unsat); + + s.dec_ref(root_lt_bvar); + s.dec_ref(gt_lit); std::cout << "=== END tst_explain_p6236 ===\n\n"; }