mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-06 15:25:46 +00:00
Code Activity

restore qfnia_tactic.cpp to expose a bug

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-02-08 16:51:53 -08:00
parent 45ea23be21
commit 2bab591ef3
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2292,6 +2292,7 @@ struct solver::imp {
} }
} }
mk_ineq(m.var(), (sign.is_pos()? llc::GT : llc ::LT), current_lemma()); mk_ineq(m.var(), (sign.is_pos()? llc::GT : llc ::LT), current_lemma());
TRACE("nla_solver", print_lemma_and_expl(tout););
} }
bool generate_simple_tangent_lemma(const rooted_mon* rm) { bool generate_simple_tangent_lemma(const rooted_mon* rm) {