handle exception internally, avoid passing rationals to integer opera…

…tions
Z3Prover · Jan 29, 2025 · fe5d17d · fe5d17d
1 parent 5b175c1
commit fe5d17d
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 2 deletions.
diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp
@@ -586,6 +586,8 @@ namespace sls {
                 if (mx == 0)
                     continue;
                 auto valmx = divide(x, val, mx);
+                if (p > 1 && !is_int(x))
+                    continue;
                 auto r = root_of(p, valmx);
                 add_update(x, r - value(x));
                 if (p % 2 == 0)
@@ -1786,7 +1788,9 @@ namespace sls {
                 // val / mx = x^p
                 if (mx == 0)
                     continue;
-                auto valmx = divide(x, val, mx);
+                if (p > 1 && !is_int(x))
+                    continue;
+                auto valmx = divide(x, val, mx);               
                 auto r = root_of(p, valmx);
                 add_update(x, r - value(x));
                 if (p % 2 == 0) 

diff --git a/src/ast/sls/sls_smt_plugin.cpp b/src/ast/sls/sls_smt_plugin.cpp
@@ -101,7 +101,13 @@ namespace sls {
     void smt_plugin::run() {
         if (!m_ddfw)
             return;
-        m_result = m_ddfw->check(0, nullptr);
+        try {
+            m_result = m_ddfw->check(0, nullptr);
+        }
+        catch (std::exception& ex) {
+            IF_VERBOSE(0, verbose_stream() << "sls-exception " << ex.what() << "\n");
+            m_result = l_undef;
+        }
         IF_VERBOSE(3, verbose_stream() << "sls-result " << m_result << "\n");
         for (auto v : m_shared_bool_vars) {
             auto w = m_smt_bool_var2sls_bool_var[v];