From cbef183ae50181ce8f3b962cab9d97f51669d089 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 20 Apr 2024 14:57:04 -0400 Subject: [PATCH] type check equality injectivity axiom Signed-off-by: Nikolaj Bjorner --- src/sat/smt/intblast_solver.cpp | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp index 33c9980411..421966377c 100644 --- a/src/sat/smt/intblast_solver.cpp +++ b/src/sat/smt/intblast_solver.cpp @@ -437,10 +437,12 @@ namespace intblast { continue; if (sib->get_arg(0)->get_root() == r1) continue; - auto a = eq_internalize(n, sib); - auto b = eq_internalize(sib->get_arg(0), n->get_arg(0)); - ctx.mark_relevant(a); - ctx.mark_relevant(b); + if (bv.get_bv_size(r1->get_expr()) != bv.get_bv_size(sib->get_arg(0)->get_expr())) + continue; + auto a = eq_internalize(n, sib); + auto b = eq_internalize(sib->get_arg(0), n->get_arg(0)); + ctx.mark_relevant(a); + ctx.mark_relevant(b); add_clause(~a, b, nullptr); return sat::check_result::CR_CONTINUE; }