fixes to githup issue Z3Prover#133 and stackoverflow reported bug on …

…assertion violation in poly_simplifier_plugin Signed-off-by: Nikolaj Bjorner <[email protected]>
wintersteiger · Jun 24, 2015 · bfb724f · bfb724f
1 parent f260eb2
commit bfb724f
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 3 deletions.
diff --git a/src/ast/simplifier/poly_simplifier_plugin.cpp b/src/ast/simplifier/poly_simplifier_plugin.cpp
@@ -69,14 +69,20 @@ expr * poly_simplifier_plugin::mk_mul(unsigned num_args, expr * const * args) {
 }
 
 expr * poly_simplifier_plugin::mk_mul(numeral const & c, expr * body) {
-    numeral c_prime;
+    numeral c_prime, d;
     c_prime = norm(c);
     if (c_prime.is_zero())
         return 0;
     if (body == 0)
         return mk_numeral(c_prime);
     if (c_prime.is_one())
-        return body;
+         return body;
+    if (is_numeral(body, d)) {
+        c_prime = norm(c_prime*d);
+        if (c_prime.is_zero())
+            return 0;
+        return mk_numeral(c_prime);
+    }
     set_curr_sort(body);
     expr * args[2] = { mk_numeral(c_prime), body };
     return mk_mul(2, args);

diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
@@ -46,7 +46,9 @@ namespace opt {
         m_dump_benchmarks(false),
         m_first(true) {
         m_params.updt_params(p);
-        m_params.m_relevancy_lvl = 0;
+        if (m_params.m_case_split_strategy == CS_ACTIVITY_DELAY_NEW) {
+            m_params.m_relevancy_lvl = 0;
+        }
     }
 
     unsigned opt_solver::m_dump_count = 0;