Skip to content
Snippets Groups Projects
Commit f173c898 authored by Mikaël Mayer's avatar Mikaël Mayer
Browse files

Correct bug generating endless loops for false-guarded test cases.

parent 7c930ebe
No related branches found
No related tags found
No related merge requests found
......@@ -199,8 +199,10 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
case None =>
true
}
(for {
if(cs.optGuard == Some(BooleanLiteral(false))) {
Nil
} else (for {
inst <- instantiations.toSeq
inR = replaceFromIDs(inst, pattExpr)
outR = replaceFromIDs(inst, doSubstitute(ieMap, cs.rhs))
......
......@@ -24,12 +24,30 @@ object DoubleListRender {
a == b || a == c || b == c
} holds
def AtoString(a : A): String = {
def mutual_lists(a : A): String = {
???
} ensuring {
(res : String) => (a, res) passes {
case B(BB(N(), BB(B(NN(), B(NN(), N())), NN())), N()) =>
"[([], [(), ()])]"
case N() =>
"[]"
case B(NN(), N()) =>
"[()]"
case B(NN(), B(NN(), N())) =>
"[(), ()]"
case B(BB(N(), NN()), N()) =>
"[([])]"
case B(NN(), B(NN(), B(NN(), N()))) =>
"[(), (), ()]"
case B(BB(N(), BB(N(), NN())), N()) =>
"[([], [])]"
case B(NN(), B(BB(N(), NN()), N())) =>
"[(), ([])]"
case B(BB(N(), NN()), B(NN(), N())) =>
"[([]), ()]"
case B(BB(B(NN(), N()), NN()), N()) =>
"[([()])]"
case B(BB(N(), BB(N(), BB(N(), NN()))), N()) =>
"[([], [], [])]"
}
}
}
\ No newline at end of file
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment