diff --git a/src/test/resources/regression/synthesis/Holes/Hole1.scala b/src/test/resources/regression/synthesis/Holes/Hole1.scala new file mode 100644 index 0000000000000000000000000000000000000000..785271b224098581bcb934c47aa89eb6e081085b --- /dev/null +++ b/src/test/resources/regression/synthesis/Holes/Hole1.scala @@ -0,0 +1,35 @@ +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 + } +}