From 0859be5649222241b385f53f1592d3d2000537f6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 25 Oct 2023 09:06:57 -0700 Subject: [PATCH] #6953 Signed-off-by: Nikolaj Bjorner --- .../rewriter/bit_blaster/bit_blaster_rewriter.cpp | 12 +++++++++++- src/sat/smt/arith_solver.cpp | 7 ------- 2 files changed, 11 insertions(+), 8 deletions(-) diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp index 801ebf4b5..68e3825c9 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp +++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp @@ -21,6 +21,7 @@ Notes: #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 index cbccf7fa8..196895216 100644 --- 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;