From 741f179c8d7c6bfd62293b15b284aae0bc994006 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Fri, 21 Nov 2014 13:59:32 +0100
Subject: [PATCH] Disallowed zero-arg smtlib FunctionApplications and updated
smtlib version
---
src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala | 10 ++++++----
1 file changed, 6 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 536ad9e00..d55f225bc 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -460,10 +460,12 @@ trait SMTLIBTarget {
case (_: Or) => Core.Or(sub.map(toSMT): _*)
case (_: IfExpr) => Core.ITE(toSMT(sub(0)), toSMT(sub(1)), toSMT(sub(2)))
case (f: FunctionInvocation) =>
- FunctionApplication(
- declareFunction(f.tfd),
- sub.map(toSMT)
- )
+ if (sub.isEmpty) declareFunction(f.tfd) else {
+ FunctionApplication(
+ declareFunction(f.tfd),
+ sub.map(toSMT)
+ )
+ }
case _ => reporter.fatalError("Unhandled nary "+e)
}
--
GitLab