From 2591fc2d5cd5098edffcc88c64860aab4d0e70d3 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Wed, 18 Feb 2015 00:12:41 +0100
Subject: [PATCH] Verify the solution by first placing it in the resulting
program
---
src/main/scala/leon/repair/Repairman.scala | 5 +++--
1 file changed, 3 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 1003e6f0e..31abd59c1 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -121,9 +121,10 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
// Validate solution if not trusted
if (!sol.isTrusted) {
reporter.info("Found untrusted solution! Verifying...")
- val (npr, fds) = synth.solutionToProgram(sol)
+ val expr = sol.toSimplifiedExpr(ctx, program)
+ ci.ch.impl = Some(expr)
- getVerificationCounterExamples(fds.head, npr) match {
+ getVerificationCounterExamples(ci.fd, program) match {
case NotValid(_, ces) if !ces.isEmpty =>
reporter.error("I ended up finding this counter example:\n"+ces.mkString(" | "))
--
GitLab