From a73fd2a501d7c6611edcd964368e88bdebff9277 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Sun, 15 Mar 2015 15:33:16 +0100
Subject: [PATCH] Fixed some tupleWrap issues
---
src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala | 2 +-
src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala | 4 ++--
2 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
index 6ab9422e8..2d88f4f34 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
@@ -91,7 +91,7 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
def encodeMapType(tpe: TypeTree): TypeTree = tpe match {
case MapType(from, to) =>
- TupleType(Seq(SetType(from), RawArrayType(from, to)))
+ tupleTypeWrap(Seq(SetType(from), RawArrayType(from, to)))
case _ => sys.error("Woot")
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 8a5b486c6..3566b165b 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -57,7 +57,7 @@ trait SMTLIBTarget {
def normalizeType(t: TypeTree): TypeTree = t match {
case ct: ClassType if ct.parent.isDefined => ct.parent.get
- case tt: TupleType => TupleType(tt.bases.map(normalizeType))
+ case tt: TupleType => tupleTypeWrap(tt.bases.map(normalizeType))
case _ => t
}
@@ -435,7 +435,7 @@ trait SMTLIBTarget {
* ===== Everything else =====
*/
case ap @ Application(caller, args) =>
- ArraysEx.Select(toSMT(caller), toSMT(Tuple(args)))
+ ArraysEx.Select(toSMT(caller), toSMT(tupleWrap(args)))
case e @ UnaryOperator(u, _) =>
e match {
--
GitLab