Commit 5e41de33 authored by Christian Müller's avatar Christian Müller

fix tests

parent 3e408548
...@@ -47,15 +47,6 @@ object Z3BSFO extends LazyLogging { ...@@ -47,15 +47,6 @@ object Z3BSFO extends LazyLogging {
logger.warn(s"Z3-BSFO: Status unknown - ${s.getReasonUnknown()}") logger.warn(s"Z3-BSFO: Status unknown - ${s.getReasonUnknown()}")
} }
// in debug mode, check if same result
if (Utils.DEBUG_MODE && f.isUniversal) {
val (c1, s1) = Z3QFree.checkUniversal(f)
if (c1 != c) {
logger.error("Different results from QFree and BSFO")
}
}
(c, s) (c, s)
} }
logger.debug(s"Z3-BSFO call took $time ms") logger.debug(s"Z3-BSFO call took $time ms")
......
...@@ -202,10 +202,11 @@ object Z3FOEncoding extends LazyLogging { ...@@ -202,10 +202,11 @@ object Z3FOEncoding extends LazyLogging {
Forall(vars, inner) Forall(vars, inner)
} }
} }
case f2 if f2.isVar() || f2.isConst() => { // There are no boolean constants, these are all function applications
case f2 if f2.isVar || (f2.isConst && !f2.isBool) => {
mapbackToVar(f2) mapbackToVar(f2)
} }
// Why is a a constant also isApp? // Why is a constant also isApp?
case f2 if f2.isApp() => { case f2 if f2.isApp() => {
val name = FunNameFromVar.unapply(f2.getFuncDecl().getName.toString) val name = FunNameFromVar.unapply(f2.getFuncDecl().getName.toString)
if (name.isEmpty) { if (name.isEmpty) {
......
...@@ -33,7 +33,7 @@ class Z3BSFOTest extends FlatSpec with LazyLogging { ...@@ -33,7 +33,7 @@ class Z3BSFOTest extends FlatSpec with LazyLogging {
} }
it should "check equalities" in { it should "check equalities" in {
val easyForm = Forall(List("x","y"), Equiv("x", "y")) val easyForm = Forall(List("x","y"), Equal("x", "y"))
val (s, solver) = Z3BSFO.checkAE(easyForm) val (s, solver) = Z3BSFO.checkAE(easyForm)
...@@ -42,7 +42,7 @@ class Z3BSFOTest extends FlatSpec with LazyLogging { ...@@ -42,7 +42,7 @@ class Z3BSFOTest extends FlatSpec with LazyLogging {
} }
it should "check disequalities" in { it should "check disequalities" in {
val easyForm = Forall(List("x","y"), Neg(Equiv("x", "y"))) val easyForm = Forall(List("x","y"), Neg(Equal("x", "y")))
val (s, solver) = Z3BSFO.checkAE(easyForm) val (s, solver) = Z3BSFO.checkAE(easyForm)
......
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