From 156bb607e7574ca18096e0dc9354b935c0d95152 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 21 Apr 2016 10:52:37 +0200
Subject: [PATCH] Filter tests with PC in CEGIS
---
src/main/scala/leon/synthesis/rules/CEGISLike.scala | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 24a201078..3f2b23292 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -695,7 +695,7 @@ abstract class CEGISLike(name: String) extends Rule(name) {
timers.cex.start()
val solverf = SolverFactory.getFromSettings(hctx, programCTree).withTimeout(cexSolverTo)
val solver = solverf.getNewSolver()
- val cnstr = FunctionInvocation(phiFd.typed, phiFd.params.map(_.id.toVariable))
+ val cnstr = FunctionInvocation(phiFd.typed, phiFd.params.map(_.id.toVariable))
try {
solver.assertCnstr(andJoin(bsOrdered.map(b => if (bs(b)) b.toVariable else Not(b.toVariable))))
@@ -772,7 +772,7 @@ abstract class CEGISLike(name: String) extends Rule(name) {
}
}
- val baseExampleInputs = p.eb.examples ++ solverExample
+ val baseExampleInputs = p.qeb.filterIns(p.pc.fullClause).eb.examples ++ solverExample
ifDebug { debug =>
baseExampleInputs.foreach { in =>
--
GitLab