mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-30 04:15:51 +00:00
Code Activity

fix bug in difference logic recognizer, assert in proof_util

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-12-11 17:01:00 -08:00
parent 299c5eb947
commit 639f902ad1
2 changed files with 8 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/muz_qe/pdr_util.cpp
View file

@ -1129,7 +1129,11 @@ namespace pdr {
if (a.is_numeral(lhs) || a.is_numeral(rhs)) {
return test_ineq(e);
}
return test_term(lhs) && test_term(rhs);
return
test_term(lhs) &&
test_term(rhs) &&
!a.is_mul(lhs) &&
!a.is_mul(rhs);
}
bool test_term(expr* e) const {

5
src/muz_qe/proof_utils.cpp
View file

@ -312,9 +312,10 @@ public:
};
void proof_utils::reduce_hypotheses(proof_ref& pr) {
class reduce_hypotheses reduce(pr.get_manager());
ast_manager& m = pr.get_manager();
class reduce_hypotheses reduce(m);
reduce(pr);
SASSERT(is_closed(pr.get_manager(), pr));
CTRACE("proof_utils", !is_closed(m, pr), tout << mk_pp(pr, m) << "\n";);
}
class proof_is_closed {