From bfab9b4bbd22123f3c332e6d39fe2a29c6231d6c Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Fri, 15 Apr 2016 13:47:31 +0200
Subject: [PATCH] fix orb
---
src/main/scala/leon/invariant/structure/Formula.scala | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/invariant/structure/Formula.scala b/src/main/scala/leon/invariant/structure/Formula.scala
index f760289d5..2480b75c5 100644
--- a/src/main/scala/leon/invariant/structure/Formula.scala
+++ b/src/main/scala/leon/invariant/structure/Formula.scala
@@ -149,12 +149,12 @@ class Formula(val fd: FunDef, initexpr: Expr, ctx: InferenceContext, initSpecCal
case Operator(args, op) =>
op(args.map(rec(_)(true)))
}
- val f1 = rec(ExpressionTransformer.simplify(simplifyArithmetic(
+ val f1 = simplifyByConstructors(rec(ExpressionTransformer.simplify(simplifyArithmetic(
//TODO: this is a hack as of now. Fix this.
//Note: it is necessary to convert real literals to integers since the linear constraint cannot handle real literals
if(ctx.usereals) ExpressionTransformer.FractionalLiteralToInt(ine)
else ine
- )))(false)
+ )))(false))
val rootvar = f1 match {
case v: Variable if(conjuncts.contains(v)) => v
case v: Variable if(disjuncts.contains(v)) => throw new IllegalStateException("f1 is a disjunct guard: "+v)
--
GitLab