mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
fix rewriter loop reported in #1354
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
dbb35b951c
commit
195d81ebef
|
@ -843,6 +843,8 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul
|
|||
continue;
|
||||
if (m_util.is_numeral(arg, arg_v) && mod(arg_v, v2) == arg_v)
|
||||
continue;
|
||||
if (m().is_ite(arg))
|
||||
continue;
|
||||
// found target for rewriting
|
||||
break;
|
||||
}
|
||||
|
|
|
@ -155,7 +155,7 @@ public:
|
|||
return res;
|
||||
}
|
||||
|
||||
void scan_skolems(const ast &proof){
|
||||
void scan_skolems(const ast &proof) {
|
||||
hash_map<ast,int> memo;
|
||||
scan_skolems_rec(memo,proof, INT_MAX);
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue