mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

fix build

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-04-30 17:52:00 -07:00
parent aa1a596394
commit 1ef4354080
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/nlsat/nlsat_solver.cpp
View file

@ -2981,7 +2981,9 @@ namespace nlsat {
m_display_var(verbose_stream(), x); m_display_var(verbose_stream(), x);
display(verbose_stream() << " ", *c) << "\n"; display(verbose_stream() << " ", *c) << "\n";
bound_constraint l(x, A, B, false, c); bound_constraint l(x, A, B, false, c);
bound_constraint h(x, -A, -B, false, c); A = -A;
B = -B;
bound_constraint h(x, A, B, false, c);
apply_fm_equality(x, clauses, l, h); apply_fm_equality(x, clauses, l, h);
return true; return true;
} }