fix #6665

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Apr 2, 2023 · 5b385bd · 5b385bd
1 parent 6324db2
commit 5b385bd
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 1 deletion.
diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java
@@ -2275,7 +2275,7 @@ public void stringExample() {
 			     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
@@ -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();