#6953

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Oct 25, 2023 · 0859be5 · 0859be5
1 parent d5fe4b0
commit 0859be5
Show file tree

Hide file tree

Showing 2 changed files with 11 additions and 8 deletions.
diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
@@ -21,6 +21,7 @@ Module Name:
 #include "ast/rewriter/bit_blaster/bit_blaster_tpl_def.h"
 #include "ast/rewriter/rewriter_def.h"
 #include "ast/rewriter/bool_rewriter.h"
+#include "ast/rewriter/th_rewriter.h"
 #include "util/ref_util.h"
 #include "ast/ast_smt2_pp.h"
 
@@ -549,10 +550,19 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
             case OP_INT2BV:
             case OP_BV2INT:
                 return BR_FAILED;
-            default:
+            default:                
                 TRACE("bit_blaster", tout << "non-supported operator: " << f->get_name() << "\n";
                       for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;);
+                {
+                    expr_ref r(m().mk_app(f, num, args), m());
+                    result = r;
+                    th_rewriter rw(m());
+                    rw(result);
+                    if (!is_app(result) || to_app(result)->get_decl() != f)
+                        return BR_REWRITE_FULL;                    
+                }
                 throw_unsupported(f);
+
             }
         }
 

diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
@@ -996,9 +996,6 @@ namespace arith {
 
         TRACE("arith", ctx.display(tout););
 
-        if (!check_delayed_eqs()) 
-            return sat::check_result::CR_CONTINUE;
-
         switch (check_lia()) {
         case l_true:
             break;
@@ -1022,10 +1019,6 @@ namespace arith {
             break;
         }
 
-        if (delayed_assume_eqs()) {
-            ++m_stats.m_assume_eqs;
-            return sat::check_result::CR_CONTINUE;
-        }
         if (assume_eqs()) {
             ++m_stats.m_assume_eqs;
             return sat::check_result::CR_CONTINUE;