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

fix the tests

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-12-25 22:49:51 +05:30 • committed by Lev Nachmanson
parent 8c876b48a7
commit fe05d1a1e8
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/util/lp/nla_solver.cpp
View file

@ -1938,7 +1938,7 @@ void solver::test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0() {
lp::explanation exp; lp::explanation exp;
// set abcde = ac * bde // set abcde = ac * bde
// ac = 1, bde = 3 -> abcde = bde, but we have abcde set to 2 // ac = 1 then abcde = bde, but we have abcde < bde
s.set_column_value(lp_a, rational(4)); s.set_column_value(lp_a, rational(4));
s.set_column_value(lp_b, rational(4)); s.set_column_value(lp_b, rational(4));
s.set_column_value(lp_c, rational(4)); s.set_column_value(lp_c, rational(4));