Skip to content
Snippets Groups Projects
Commit 3707aee0 authored by Etienne Kneuss's avatar Etienne Kneuss
Browse files

Add back a few tests about Holes

parent 603f0fbb
No related branches found
No related tags found
No related merge requests found
import leon.lang._
import leon.collection._
import leon.lang.synthesis._
object Holes {
def abs1(a: Int) = {
if (?(true, false)) {
a
} else {
-a
}
} ensuring {
_ >= 0
}
def abs2(a: Int) = {
if (???[Boolean]) {
a
} else {
-a
}
} ensuring {
_ >= 0
}
def abs3(a: Int) = {
if (?(a > 0, a < 0)) {
a
} else {
-a
}
} ensuring {
_ >= 0
}
}
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