diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 93ce2f342e3d6e6b42216d5358beda94a15160c7..d9d186bd436f0859ef4f1e2d0b3346981a48de3c 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -64,17 +64,17 @@ trait SMTLIBTarget {
 
   // Corresponds to a smt map, not a leon/scala array
   // Should NEVER escape past SMT-world
-  case class RawArrayType(from: TypeTree, to: TypeTree) extends TypeTree
+  private[smtlib] case class RawArrayType(from: TypeTree, to: TypeTree) extends TypeTree
 
   // Corresponds to a raw array value, which is coerced to a Leon expr depending on target type (set/array)
   // Should NEVER escape past SMT-world
-  case class RawArrayValue(keyTpe: TypeTree, elems: Map[Expr, Expr], default: Expr) extends Expr {
+  private[smtlib] case class RawArrayValue(keyTpe: TypeTree, elems: Map[Expr, Expr], default: Expr) extends Expr {
     val getType = RawArrayType(keyTpe, default.getType)
   }
 
   def fromRawArray(r: RawArrayValue, tpe: TypeTree): Expr = tpe match {
     case SetType(base) =>
-      assert(r.default == BooleanLiteral(false) && r.keyTpe == base)
+      require(r.default == BooleanLiteral(false) && r.keyTpe == base)
 
       finiteSet(r.elems.keySet, base)