From c25975a429a030c43b949ada971f40407bdd8b26 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 3 Apr 2020 12:35:20 -0700
Subject: [PATCH] fix #3703
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/smt/theory_utvpi.cpp | 3 ---
1 file changed, 3 deletions(-)
diff --git a/src/smt/theory_utvpi.cpp b/src/smt/theory_utvpi.cpp
index 3a9f10c30..cf7dafe89 100644
--- a/src/smt/theory_utvpi.cpp
+++ b/src/smt/theory_utvpi.cpp
@@ -128,9 +128,6 @@ namespace smt {
else if (a.is_numeral(e, num)) {
m_weight += num*mul;
}
- else if (a.is_to_real(e, e1)) {
- m_terms.push_back(std::make_pair(e1, mul));
- }
else if (!is_uninterp_const(e)) {
return false;
}