From a3f7541719a809cde03f3aa453940aa4d44b0843 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 20 Jan 2025 19:04:36 -0800
Subject: [PATCH] fix #7517

---
 src/qe/mbp/mbp_arith.cpp | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/src/qe/mbp/mbp_arith.cpp b/src/qe/mbp/mbp_arith.cpp
index 8bbf3a002..5c1654a09 100644
--- a/src/qe/mbp/mbp_arith.cpp
+++ b/src/qe/mbp/mbp_arith.cpp
@@ -39,7 +39,6 @@ namespace mbp {
         bool              m_check_purified = true;  // check that variables are properly pure 
         bool              m_apply_projection = false;
 
-
         imp(ast_manager& m) :
             m(m), a(m) {}
 
@@ -275,10 +274,6 @@ namespace mbp {
                 extract_coefficients(mbo, eval, ts0, tids, coeffs);
                 mbo.add_divides(coeffs, c0, mul1);
             }
-            else if (a.is_to_real(t))
-                throw default_exception("mbp to-real");
-            else if (a.is_to_int(t))
-                throw default_exception("mbp to-int");
             else {
                 TRACE("qe", tout << "insert mul " << mk_pp(t, m) << "\n");
                 insert_mul(t, mul, ts);