From a330dede84cf976b488b0c55a63185f4f6f6caf4 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 4 Mar 2015 17:26:34 +0100
Subject: [PATCH] Some SMTLib tweaking
---
src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 93ce2f342..d9d186bd4 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)
--
GitLab