Function without args should not end up in a define-funs-rec

src/main/scala/leon/solvers/smtlib/SMTLIBUnrollingCVC4Target.scala

@@ -3,8 +3,9 @@
 package leon
 package solvers.smtlib
 
+import leon.purescala.Common.FreshIdentifier
 import leon.purescala.Expressions.Expr
-import purescala.Definitions.TypedFunDef
+import leon.purescala.Definitions.{ValDef, TypedFunDef}
 import purescala.DefOps.typedTransitiveCallees
 import leon.purescala.ExprOps.{variablesOf, matchToIfThenElse}
 import smtlib.parser.Commands._
@@ -23,11 +24,23 @@ trait SMTLIBUnrollingCVC4Target extends SMTLIBCVC4Target {
       val (funs, exploredAll) = typedTransitiveCallees(Set(tfd), Some(typedFunDefExplorationLimit))
       if (!exploredAll) {
         reporter.warning(
-          s"Did not manage to explore the space of typed functions called from ${tfd.id}. The solver may fail"
+          s"Did not manage to explore the space of typed functions trasitively called from ${tfd.id}. The solver may fail"
         )
       }
 
-      val smtFunDecls = funs.toSeq.collect {
+      val smtFunDecls = funs.toSeq.flatMap {
+        case tfd if tfd.params.isEmpty =>
+          // FIXME: Here we actually want to call super[SMTLIBCVC4Target].declareFunction(tfd),
+          // but we inline it to work around a freakish compiler bug
+          if (!functions.containsA(tfd)) {
+            val id = if (tfd.tps.isEmpty) {
+              tfd.id
+            } else {
+              FreshIdentifier(tfd.id.name)
+            }
+            sendCommand( DeclareFun(id2sym(id),Seq(),declareSort(tfd.returnType)) )
+          }
+          None
         case tfd if !functions.containsA(tfd) && tfd.params.nonEmpty =>
           val id = if (tfd.tps.isEmpty) {
             tfd.id
@@ -36,11 +49,12 @@ trait SMTLIBUnrollingCVC4Target extends SMTLIBCVC4Target {
           }
           val sym = id2sym(id)
           functions +=(tfd, sym)
-          FunDec(
+          Some(FunDec(
             sym,
             tfd.params map { p => SortedVar(id2sym(p.id), declareSort(p.getType)) },
             declareSort(tfd.returnType)
-          )
+          ))
+        case _ => None
       }
       val smtBodies = smtFunDecls map { case FunDec(sym, _, _) =>
         val tfd = functions.toA(sym)

src/test/scala/leon/test/verification/NewSolversRegression.scala

@@ -30,15 +30,15 @@ class NewSolversRegression extends VerificationRegression {
         false
     }
 
-    (
-      if (isZ3Available)
-        List(List("--solvers=smt-z3-quantified", "--feelinglucky", "--timeout=3"))
-      else Nil
-    ) ++ (
+    //(
+     // if (isZ3Available)
+        //List(List("--solvers=smt-z3-quantified", "--feelinglucky", "--timeout=3"))
+      //else Nil
+    //) ++ (
       if (isCVC4Available)
         List(List("--solvers=smt-2.5-cvc4", "--feelinglucky"))
       else Nil
-    )
+    //)
   }
   
   test()