Commit 56ee3d7e authored by Heiko Becker's avatar Heiko Becker

Fix bug in HOL4 abstract environment generation, preventing some benchmarks from succeeding

parent 12dd5cf1
......@@ -458,7 +458,7 @@ object CertificatePhase extends DaisyPhase {
case x @ _ =>
val nameE = expressionNames.get(e)
val nameE = expressionNames(e)
e match {
case x @ Variable(id) =>
......@@ -540,7 +540,7 @@ object CertificatePhase extends DaisyPhase {
case x @ _ =>
val nameE = expressionNames.get(e)
val nameE = expressionNames(e)
e match {
case x @ Variable(id) =>
......@@ -577,7 +577,7 @@ object CertificatePhase extends DaisyPhase {
conditional (
"( e = " + nameE + " )",
"(" + intvE + ", " + errE + ")",
lFun)
rFun)
case x @ Times(lhs, rhs) =>
val lFun = hol4AbsEnv (lhs, errorMap, rangeMap, cont)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment