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();