From 71ad4bf8991bb319b53b4a52ed6cfaa3064cd7ee Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 12 Nov 2012 17:00:54 +0100
Subject: [PATCH] Re-implement Assert using C
---
src/main/scala/leon/synthesis/Rules.scala | 15 +++------------
1 file changed, 3 insertions(+), 12 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 1af93b194..fc711b1e7 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -144,18 +144,9 @@ class Assert(synth: Synthesizer) extends Rule("Assert", synth, 200) {
if (others.isEmpty) {
RuleSuccess(Solution(And(exprsA), Tuple(p.xs.map(id => simplestValue(Variable(id))))))
} else {
- /*
- * Disable for now, it is not that useful anyway
- val onSuccess: List[Solution] => Solution = {
- case List(s) => Solution(And(s.pre +: exprsA), s.term)
- case _ => Solution.none
- }
-
- val sub = p.copy(phi = And(others))
-
- RuleStep(List(sub), onSuccess)
- */
- RuleInapplicable
+ val sub = p.copy(c = And(p.c +: exprsA), phi = And(others))
+
+ RuleStep(List(sub), forward)
}
} else {
RuleInapplicable
--
GitLab