inox
inox copied to clipboard
Published
20 hours ago •
epfl-lara
epfl-lara
StackOverflowError on an equivalence checking example
The following (minimized) equivalence checking example crashes with a StackOverflowError:
import stainless.lang._
object C_mem_sol1 {
sealed abstract class Formula {}
case class True() extends Formula
case class Imply(p1: Formula, p2: Formula) extends Formula
def eval1(f: Formula): Boolean = {
f match {
case True() => true
case Imply(p1, p2) => true // modified, for simplification
}
}
def eval(f: Formula): Boolean = {
f match {
case True() => true
case Imply(f1, f2) => {
(eval(f1), eval(f2)) match {
case (true, true) => true
case (true, false) => false
case (false, true) => true
case (false, false) => true
}
}
}
}
def eval_template(f: Formula): Boolean = {
f match {
case True() => { true }
case Imply(f1, f2) => {
(eval_template(f1), eval_template(f2)) match {
case (true, true) => true
case (true, false) => false
case (false, true) => true
case (false, false) => true
}
}
}
} ensuring(_ => eval(f) == eval1(f))
}
Stack trace:
java.lang.StackOverflowError at inox.ast.Definitions$$anon$1.convert(Definitions.scala:70) at inox.ast.Definitions$$anon$1.convert(Definitions.scala:67) at inox.ast.Definitions$VariableSymbol.to(Definitions.scala:50) at inox.ast.Definitions$VariableSymbol.to$(Definitions.scala:50) at inox.ast.Expressions$Variable.to(Expressions.scala:46) at inox.ast.Expressions$Variable.toVal(Expressions.scala:50) at inox.transformers.Transformer.$anonfun$transform$3(Transformer.scala:63) at scala.collection.immutable.List.map(List.scala:293) at inox.transformers.Transformer.transform(Transformer.scala:62) at inox.transformers.Transformer.transform$(Transformer.scala:51) at inox.ast.SymbolOps$$anon$1.inox$transformers$SimplifierWithPC$$super$transform(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:307) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:163) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.$anonfun$simplify$18(SimplifierWithPC.scala:267) at scala.collection.immutable.List.map(List.scala:293) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:267) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.$anonfun$simplify$26(SimplifierWithPC.scala:278) at scala.collection.immutable.List.map(List.scala:293) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:278) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:207) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.$anonfun$simplifyAndCons$1(SimplifierWithPC.scala:316) at scala.collection.immutable.List.map(List.scala:293) at inox.transformers.SimplifierWithPC.simplifyAndCons(SimplifierWithPC.scala:316) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:271) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:107) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:131) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:136) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:233) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:136) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:219) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:232) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.isPure(SimplifierWithPC.scala:90) at inox.transformers.SimplifierWithPC.isPure$(SimplifierWithPC.scala:90) at inox.ast.SymbolOps$$anon$1.isPure(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.isPureFunction(SimplifierWithPC.scala:63) at inox.transformers.SimplifierWithPC.isPureFunction$(SimplifierWithPC.scala:54) at inox.ast.SymbolOps$$anon$1.isPureFunction(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:268) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:232) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.$anonfun$simplifyAndCons$1(SimplifierWithPC.scala:316) at scala.collection.immutable.List.map(List.scala:293) at inox.transformers.SimplifierWithPC.simplifyAndCons(SimplifierWithPC.scala:316) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:271) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:107) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.isPure(SimplifierWithPC.scala:90) at inox.transformers.SimplifierWithPC.isPure$(SimplifierWithPC.scala:90) at inox.ast.SymbolOps$$anon$1.isPure(SymbolOps.scala:33) at inox.ast.SymbolOps.isPureIn(SymbolOps.scala:215) at inox.ast.SymbolOps.isPureIn$(SymbolOps.scala:207) at inox.ast.SimpleSymbols$SimpleSymbols.isPureIn(SimpleSymbols.scala:12) at inox.ast.SymbolOps.isPure(SymbolOps.scala:202) at inox.ast.SymbolOps.isPure$(SymbolOps.scala:202) at inox.ast.SimpleSymbols$SimpleSymbols.isPure(SimpleSymbols.scala:12) at inox.ast.SymbolOps.isAlwaysPure(SymbolOps.scala:204) at inox.ast.SymbolOps.isAlwaysPure$(SymbolOps.scala:204) at inox.ast.SimpleSymbols$SimpleSymbols.isAlwaysPure(SimpleSymbols.scala:12) at inox.ast.SymbolOps.ifExpr(SymbolOps.scala:1183) at inox.ast.SymbolOps.ifExpr$(SymbolOps.scala:1182) at inox.ast.SimpleSymbols$SimpleSymbols.ifExpr(SimpleSymbols.scala:12) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:140) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:136) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:136) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:233) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:136) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:219) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:232) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.isPure(SimplifierWithPC.scala:90) at inox.transformers.SimplifierWithPC.isPure$(SimplifierWithPC.scala:90) at inox.ast.SymbolOps$$anon$1.isPure(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.isPureFunction(SimplifierWithPC.scala:63) at inox.transformers.SimplifierWithPC.isPureFunction$(SimplifierWithPC.scala:54) at inox.ast.SymbolOps$$anon$1.isPureFunction(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:268) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:232) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.$anonfun$simplifyAndCons$1(SimplifierWithPC.scala:316) at scala.collection.immutable.List.map(List.scala:293) at inox.transformers.SimplifierWithPC.simplifyAndCons(SimplifierWithPC.scala:316) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:271) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:107) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.isPure(SimplifierWithPC.scala:90) at inox.transformers.SimplifierWithPC.isPure$(SimplifierWithPC.scala:90) at inox.ast.SymbolOps$$anon$1.isPure(SymbolOps.scala:33) at inox.ast.SymbolOps.isPureIn(SymbolOps.scala:215) at inox.ast.SymbolOps.isPureIn$(SymbolOps.scala:207) at inox.ast.SimpleSymbols$SimpleSymbols.isPureIn(SimpleSymbols.scala:12) at inox.ast.SymbolOps.isPure(SymbolOps.scala:202) at inox.ast.SymbolOps.isPure$(SymbolOps.scala:202) at inox.ast.SimpleSymbols$SimpleSymbols.isPure(SimpleSymbols.scala:12) at inox.ast.SymbolOps.isAlwaysPure(SymbolOps.scala:204) at inox.ast.SymbolOps.isAlwaysPure$(SymbolOps.scala:204) at inox.ast.SimpleSymbols$SimpleSymbols.isAlwaysPure(SimpleSymbols.scala:12) at inox.ast.SymbolOps.ifExpr(SymbolOps.scala:1183) at inox.ast.SymbolOps.ifExpr$(SymbolOps.scala:1182) at inox.ast.SimpleSymbols$SimpleSymbols.ifExpr(SimpleSymbols.scala:12) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:140) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:136) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:136) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:233) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:136) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:219) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:232) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.isPure(SimplifierWithPC.scala:90) at inox.transformers.SimplifierWithPC.isPure$(SimplifierWithPC.scala:90) at inox.ast.SymbolOps$$anon$1.isPure(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.isPureFunction(SimplifierWithPC.scala:63) at inox.transformers.SimplifierWithPC.isPureFunction$(SimplifierWithPC.scala:54) at inox.ast.SymbolOps$$anon$1.isPureFunction(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:268) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:232) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.$anonfun$simplifyAndCons$1(SimplifierWithPC.scala:316) at scala.collection.immutable.List.map(List.scala:293) at inox.transformers.SimplifierWithPC.simplifyAndCons(SimplifierWithPC.scala:316) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:271) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.simplify(SimplifierWithPC.scala:107) at inox.transformers.SimplifierWithPC.simplify$(SimplifierWithPC.scala:92) at inox.ast.SymbolOps$$anon$1.simplify(SymbolOps.scala:33) at inox.transformers.SimplifierWithPC.isPure(SimplifierWithPC.scala:90) at inox.transformers.SimplifierWithPC.isPure$(SimplifierWithPC.scala:90) at inox.ast.SymbolOps$$anon$1.isPure(SymbolOps.scala:33) at inox.ast.SymbolOps.isPureIn(SymbolOps.scala:215) at inox.ast.SymbolOps.isPureIn$(SymbolOps.scala:207) at inox.ast.SimpleSymbols$SimpleSymbols.isPureIn(SimpleSymbols.scala:12)
