mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-03 11:25:40 +00:00
Code Activity

fix lemma logging in nlsat

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2024-06-17 13:14:31 -07:00
parent e4b3df2189
commit bf3615d4fb
1 changed files with 7 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/nlsat/nlsat_solver.cpp
View file

@ -3698,10 +3698,12 @@ namespace nlsat {
std::ostream& display_smt2_arith_decls(std::ostream & out) const { std::ostream& display_smt2_arith_decls(std::ostream & out) const {
unsigned sz = m_is_int.size(); unsigned sz = m_is_int.size();
for (unsigned i = 0; i < sz; i++) { for (unsigned i = 0; i < sz; i++) {
if (is_int(i)) if (is_int(i)) {
out << "(declare-fun x" << i << " () Int)\n"; out << "(declare-fun "; m_display_var(out, i) << " () Int)\n";
else }
out << "(declare-fun x" << i << " () Real)\n"; else {
out << "(declare-fun "; m_display_var(out, i) << " () Real)\n";
}
} }
return out; return out;
} }
@ -3720,7 +3722,7 @@ namespace nlsat {
display_smt2_arith_decls(out); display_smt2_arith_decls(out);
out << "(assert (and true\n"; out << "(assert (and true\n";
for (clause* c : m_clauses) { for (clause* c : m_clauses) {
display_smt2(out, *c) << "\n"; display_smt2(out, *c, m_display_var) << "\n";
} }
out << "))\n" << std::endl; out << "))\n" << std::endl;
return out; return out;