From 195d81ebefad9ea8b38d0bf049a268ee3012f50c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 13 Nov 2017 13:49:03 -0800
Subject: [PATCH] fix rewriter loop reported in #1354
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/ast/rewriter/arith_rewriter.cpp | 2 ++
src/interp/iz3translate.cpp | 2 +-
2 files changed, 3 insertions(+), 1 deletion(-)
diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp
index 631e1d8f3..acc3b889f 100644
--- a/src/ast/rewriter/arith_rewriter.cpp
+++ b/src/ast/rewriter/arith_rewriter.cpp
@@ -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;
}
diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp
index e4730ea63..ce2249a88 100755
--- a/src/interp/iz3translate.cpp
+++ b/src/interp/iz3translate.cpp
@@ -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);
}