3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00

enforce sign coherence #4740

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-11-09 14:28:49 -08:00
parent e955bd09e5
commit 638ef9ed03
2 changed files with 7 additions and 1 deletions

View file

@ -310,7 +310,11 @@ bool order::order_lemma_on_ac_and_bc_and_factors(const monic& ac,
SASSERT(!val(c).is_zero());
rational c_sign = rational(nla::rat_sign(val(c)));
auto av_c_s = val(a) * c_sign;
auto bv_c_s = val(b) * c_sign;
auto bv_c_s = val(b) * c_sign;
if (b.sign() != a.sign())
return false;
if (bc.rsign() != ac.rsign())
return false;
if ((var_val(ac) > var_val(bc) && av_c_s < bv_c_s) ||
(var_val(ac) < var_val(bc) && av_c_s > bv_c_s)) {
generate_ol(ac, a, c, bc, b);

View file

@ -480,6 +480,8 @@ namespace smt {
#else
strm << "lemma_" << (++m_lemma_id) << ".smt2";
#endif
SASSERT(m_lemma_id != 341);
VERIFY(m_lemma_id != 341);
return strm.str();
}