mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-20 07:24:40 +00:00
Code Activity

use indexed root expressions id add_zero_assumption

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-11-18 16:35:27 -10:00 • committed by Nikolaj Bjorner
parent 50e4452e62
commit 0179ed855d
2 changed files with 44 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/nlsat/nlsat_solver.cpp
View file

@ -1139,7 +1139,7 @@ namespace nlsat {
used_vars[v] = true;
}
display(out << "(echo \"#" << m_lemma_count++ << ":" << annotation << ":", n, cls) << "\")\n";
out << "(set-logic ALL)\n";
out << "(set-logic NRA)\n";
out << "(set-option :rlimit " << m_lemma_rlimit << ")\n";
if (is_valid) {
display_smt2_bool_decls(out, used_bools);
@ -2260,7 +2260,7 @@ namespace nlsat {
}
}
out << "(echo \"#" << m_lemma_count++ << ":assignment lemma " << comment.str() << "\")\n";
out << "(set-logic ALL)\n";
out << "(set-logic NRA)\n";
out << "(set-option :rlimit " << m_lemma_rlimit << ")\n";
display_smt2_bool_decls(out, used_bools);
display_smt2_arith_decls(out, used_vars);