From a9c3f4c2e103fefe1417d5e3cf927444dac1f570 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 17 Jun 2015 20:31:04 +0200
Subject: [PATCH] Some simplifications

---
 .../leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala    | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
index ce6783574..9a949a6d7 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
@@ -78,8 +78,8 @@ abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program
       )
     }
 
-    val smtBodies = smtFunDecls map { case FunDec(sym, _, _) =>
-      val tfd = functions.toA(sym)
+    val smtBodies = smtFunDecls map { case f =>
+      val tfd = functions.toA(f.name)
       try {
         toSMT(tfd.body.get)(tfd.params.map { p =>
           (p.id, id2sym(p.id): Term)
@@ -137,7 +137,7 @@ abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program
 
     // We want to check if the negation of the vc is sat under inductive hyp.
     // So we need to see if (indHyp /\ !vc) is satisfiable
-    liftLets(matchToIfThenElse(and(andJoin(inductiveHyps), not(cond))))
+    liftLets(matchToIfThenElse(andJoin(inductiveHyps :+ not(cond))))
 
   }
 
-- 
GitLab