From a0f3727e90c4446ba2c1fa7e4392637587ad9632 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Sun, 12 Mar 2023 19:26:47 +0000 Subject: [PATCH] BV: add missing neg internalizer usually bvneg is eliminated during rewriting, but it can be left behind during e.g. a badly-timed timeout --- src/smt/theory_bv.cpp | 2 ++ src/smt/theory_bv.h | 1 + 2 files changed, 3 insertions(+) diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index b3a6e77ff..00564ed3e 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -811,6 +811,7 @@ namespace smt { init_bits(e, bits); } + MK_UNARY(internalize_neg, mk_neg); MK_UNARY(internalize_not, mk_not); MK_UNARY(internalize_redand, mk_redand); MK_UNARY(internalize_redor, mk_redor); @@ -895,6 +896,7 @@ namespace smt { } switch (term->get_decl_kind()) { case OP_BV_NUM: internalize_num(term); return true; + case OP_BNEG: internalize_neg(term); return true; case OP_BADD: internalize_add(term); return true; case OP_BSUB: internalize_sub(term); return true; case OP_BMUL: internalize_mul(term); return true; diff --git a/src/smt/theory_bv.h b/src/smt/theory_bv.h index 588f19d89..73d659c68 100644 --- a/src/smt/theory_bv.h +++ b/src/smt/theory_bv.h @@ -196,6 +196,7 @@ namespace smt { void internalize_ext_rotate_right(app * n); void internalize_and(app * n); void internalize_or(app * n); + void internalize_neg(app * n); void internalize_not(app * n); void internalize_nand(app * n); void internalize_nor(app * n);