From 71cdbf7b72efef3b8526e8c378e42b3df4f42f6d Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 13 Nov 2025 19:48:09 -1000 Subject: [PATCH] t Signed-off-by: Lev Nachmanson --- src/nlsat/nlsat_solver.cpp | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 1816bc4c8..59395284a 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -224,6 +224,7 @@ namespace nlsat { bool m_dump_mathematica; bool m_check_lemmas; unsigned m_max_conflicts; + unsigned m_lemma_rlimit; unsigned m_lemma_count; unsigned m_variable_ordering_strategy; bool m_set_0_more; @@ -271,6 +272,7 @@ namespace nlsat { reset_statistics(); mk_true_bvar(); m_lemma_count = 0; + m_lemma_rlimit = 10 * 1000; } ~imp() { @@ -1139,8 +1141,9 @@ namespace nlsat { used_vars[v] = true; } TRACE(nlsat, display(tout << "(echo \"#" << ++ttt << " expl lemma ", n, cls) << "\")\n"); - display(out << "(echo \"#" << ttt << (is_valid?" learned " : " conflict ") , n, cls) << "\")\n"; + display(out << "(echo \"#" << ttt << (is_valid ? " learned " : " conflict "), n, cls) << "\")\n"; out << "(set-logic ALL)\n"; + out << "(set-option :rlimit " << m_lemma_rlimit << ")\n"; if (is_valid) { display_smt2_bool_decls(out, used_bools); display_smt2_arith_decls(out, used_vars); @@ -2243,8 +2246,9 @@ namespace nlsat { for (var v : vars) used_vars[v] = true; } - out << "(echo \"#" << ttt<< " assignment lemma\")\n"; + out << "(echo \"#" << ttt << " assignment lemma\")\n"; out << "(set-logic ALL)\n"; + out << "(set-option :rlimit " << m_lemma_rlimit << ")\n"; display_smt2_bool_decls(out, used_bools); display_smt2_arith_decls(out, used_vars); display_bool_assignment(out, false, &used_bools);