From fd2a8a554d0fb48838a7e40f9c718f5aceff830d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 1 Feb 2025 20:04:29 -0800 Subject: [PATCH] disable small clause generation for propagation --- src/smt/theory_lra.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index cc1775153..9ee47b9b0 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2399,7 +2399,7 @@ public: VERIFY(validate_assign(lit)); if (params().m_arith_dump_lemmas) dump_assign_lemma(lit); - if (core.size() < small_lemma_size() && eqs.empty()) { + if (false && core.size() < small_lemma_size() && eqs.empty()) { m_core2.reset(); for (auto const& c : core) { m_core2.push_back(~c);