From 6f37da5a0797278590f082aa22024f281dece8e0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 26 Oct 2024 14:56:38 -0700 Subject: [PATCH] validate sls-arith lemmas Signed-off-by: Nikolaj Bjorner --- src/sat/smt/arith_solver.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index a3ee5408c..fe5372e7a 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -1272,6 +1272,8 @@ namespace arith { for (literal& c : m_core) c.neg(); DEBUG_CODE(for (literal c : m_core) { SASSERT(s().value(c) != l_true); }); + + for (literal c : m_core) { VERIFY(s().value(c) != l_true); } add_redundant(m_core, explain(ty)); }