From 799fc9e8c4d7b3e5e91bdb14b2810bb2a787f21f Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 18 Feb 2026 10:59:41 -1000 Subject: [PATCH] hook up a test Signed-off-by: Lev Nachmanson --- src/test/nlsat.cpp | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) diff --git a/src/test/nlsat.cpp b/src/test/nlsat.cpp index 4a6d65beb..81d0cab9e 100644 --- a/src/test/nlsat.cpp +++ b/src/test/nlsat.cpp @@ -466,16 +466,6 @@ static void project_fa(nlsat::solver& s, nlsat::explain& ex, nlsat::var x, unsig std::cout << ")\n"; } -static bool literal_holds(nlsat::solver& s, nlsat::evaluator& eval, nlsat::literal l) { - if (l == nlsat::true_literal) - return true; - if (l == nlsat::false_literal) - return false; - nlsat::atom* a = s.bool_var2atom(l.var()); - ENSURE(a != nullptr); - return eval.eval(a, l.sign()); -} - static nlsat::literal mk_gt(nlsat::solver& s, nlsat::poly* p) { nlsat::poly * _p[1] = { p }; bool is_even[1] = { false }; @@ -2492,6 +2482,8 @@ static void tst_explain_p6236() { } void tst_nlsat() { + tst_unsound_gh8397(); + std::cout << "------------------\n"; tst_explain_p6236(); std::cout << "------------------\n"; tst_unsound_lws_disc_zero();