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

fix assertion violation in nlsat test

Browse source
This commit is contained in:
Nuno Lopes 2019-06-13 16:36:03 +01:00
parent 94d2a16282
commit 46d23ea8d7
1 changed files with 3 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/test/nlsat.cpp
View file

@ -282,7 +282,6 @@ static void tst5() {
nlsat::var x0, x1; nlsat::var x0, x1;
x0 = pm.mk_var(); x0 = pm.mk_var();
x1 = pm.mk_var(); x1 = pm.mk_var();
nlsat::interval_set_ref i(ism);
polynomial_ref p(pm); polynomial_ref p(pm);
polynomial_ref _x0(pm), _x1(pm); polynomial_ref _x0(pm), _x1(pm);
@ -297,11 +296,11 @@ static void tst5() {
scoped_anum zero(am); scoped_anum zero(am);
am.set(zero, 0); am.set(zero, 0);
as.set(0, zero); as.set(0, zero);
i = ev.infeasible_intervals(a, true); auto i = ev.infeasible_intervals(a, true);
std::cout << "1) " << i << "\n"; std::cout << "1) " << i << "\n";
as.set(1, zero); as.set(1, zero);
i = ev.infeasible_intervals(a, true); auto i2 = ev.infeasible_intervals(a, true);
std::cout << "2) " << i << "\n"; std::cout << "2) " << i2 << "\n";
} }