mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
parent
d5fe4b0d78
commit
0859be5649
|
@ -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);
|
||||
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -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;
|
||||
|
|
Loading…
Reference in a new issue