mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-23 06:01:26 +00:00
Code Activity

t

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-11-13 19:43:58 -10:00
parent eba6a66e6f
commit d0e139f2b3
1 changed files with 5 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/nlsat/nlsat_solver.cpp
View file

@ -3685,6 +3685,11 @@ namespace nlsat {
out << " (< " << y1 << " " << y2 << ")\n"; out << " (< " << y1 << " " << y2 << ")\n";
} }
auto y0 = mk_y_name(0);
out << " (forall ((y Real)) (=> (< y " << y0 << ") (not (= ";
printer(out, "y");
out << " 0))))\n";
for (unsigned j = 0; j + 1 < idx; ++j) { for (unsigned j = 0; j + 1 < idx; ++j) {
auto y1 = mk_y_name(j); auto y1 = mk_y_name(j);
auto y2 = mk_y_name(j + 1); auto y2 = mk_y_name(j + 1);