From 92b5806a93882d9f53ec1105f1078a5c887f832a Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 16 Mar 2015 14:39:38 +0100
Subject: [PATCH] Use tupleTypeWrap in SMTLib
---
src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala | 2 +-
src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
index 3c6fb95d8..ed5559a41 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
@@ -64,7 +64,7 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
case (FunctionApplication(SimpleSymbol(SSymbol("store")), Seq(arr, key, elem)), ft @ FunctionType(from,to)) =>
val FiniteLambda(dflt, mapping) = fromSMT(arr, tpe)
- finiteLambda(dflt, mapping :+ (fromSMT(key, TupleType(from)) -> fromSMT(elem, to)), from)
+ finiteLambda(dflt, mapping :+ (fromSMT(key, tupleTypeWrap(from)) -> fromSMT(elem, to)), from)
case (FunctionApplication(SimpleSymbol(SSymbol("singleton")), elems), SetType(base)) =>
finiteSet(elems.map(fromSMT(_, base)).toSet, base)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index d9d186bd4..91a074d5e 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -106,7 +106,7 @@ trait SMTLIBTarget {
declareMapSort(from, to)
case FunctionType(from, to) =>
- Sort(SMTIdentifier(SSymbol("Array")), Seq(declareSort(TupleType(from)), declareSort(to)))
+ Sort(SMTIdentifier(SSymbol("Array")), Seq(declareSort(tupleTypeWrap(from)), declareSort(to)))
case TypeParameter(id) =>
val s = id2sym(id)
--
GitLab