Skip to content
Snippets Groups Projects
Commit 1e41ae11 authored by Regis Blanc's avatar Regis Blanc
Browse files

fix orb

parent acbfac7e
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/main/scala/leon/invariant/structure/Formula.scala
+ 2
− 2
View file @ 1e41ae11
...@@ -149,12 +149,12 @@ class Formula(val fd: FunDef, initexpr: Expr, ctx: InferenceContext, initSpecCal ...@@ -149,12 +149,12 @@ class Formula(val fd: FunDef, initexpr: Expr, ctx: InferenceContext, initSpecCal
case Operator(args, op) => case Operator(args, op) =>
op(args.map(rec(_)(true))) 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. //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 //Note: it is necessary to convert real literals to integers since the linear constraint cannot handle real literals
if(ctx.usereals) ExpressionTransformer.FractionalLiteralToInt(ine) if(ctx.usereals) ExpressionTransformer.FractionalLiteralToInt(ine)
else ine else ine
)))(false) )))(false))
val rootvar = f1 match { val rootvar = f1 match {
case v: Variable if(conjuncts.contains(v)) => v case v: Variable if(conjuncts.contains(v)) => v
case v: Variable if(disjuncts.contains(v)) => throw new IllegalStateException("f1 is a disjunct guard: "+v) case v: Variable if(disjuncts.contains(v)) => throw new IllegalStateException("f1 is a disjunct guard: "+v)
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment