From bf3615d4fbc017f0da036ac2fe3a3dce09922cd9 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Mon, 17 Jun 2024 13:14:31 -0700 Subject: [PATCH] fix lemma logging in nlsat Signed-off-by: Lev Nachmanson --- src/nlsat/nlsat_solver.cpp | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index ca057afef..26c2f617b 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -3698,10 +3698,12 @@ namespace nlsat { std::ostream& display_smt2_arith_decls(std::ostream & out) const { unsigned sz = m_is_int.size(); for (unsigned i = 0; i < sz; i++) { - if (is_int(i)) - out << "(declare-fun x" << i << " () Int)\n"; - else - out << "(declare-fun x" << i << " () Real)\n"; + if (is_int(i)) { + out << "(declare-fun "; m_display_var(out, i) << " () Int)\n"; + } + else { + out << "(declare-fun "; m_display_var(out, i) << " () Real)\n"; + } } return out; } @@ -3720,7 +3722,7 @@ namespace nlsat { display_smt2_arith_decls(out); out << "(assert (and true\n"; for (clause* c : m_clauses) { - display_smt2(out, *c) << "\n"; + display_smt2(out, *c, m_display_var) << "\n"; } out << "))\n" << std::endl; return out;