From 5b385bd2fe03f781e0e59e25139006ae8d9354ce Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 2 Apr 2023 10:58:01 -0700 Subject: [PATCH] fix #6665 Signed-off-by: Nikolaj Bjorner --- examples/java/JavaExample.java | 2 +- src/smt/theory_bv.cpp | 3 +++ 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java index f6f171c46..a27a60721 100644 --- a/examples/java/JavaExample.java +++ b/examples/java/JavaExample.java @@ -2275,7 +2275,7 @@ class JavaExample ctx.mkToRe(ctx.mkString("d"))); System.out.println(c); - } + } public static void main(String[] args) { diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 00564ed3e..7adab35f4 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -946,6 +946,9 @@ namespace smt { internalize_bv2int(term); } return params().m_bv_enable_int2bv2int; + case OP_BSREM: return false; + case OP_BUREM: return false; + case OP_BSMOD: return false; default: TRACE("bv_op", tout << "unsupported operator: " << mk_ll_pp(term, m) << "\n";); UNREACHABLE();