diff --git a/testcases/synthesis/ScaleWeight.scala b/testcases/synthesis/ScaleWeight.scala new file mode 100644 index 0000000000000000000000000000000000000000..7e1c0f2eadc11294b9301b07f8908d33dec43c03 --- /dev/null +++ b/testcases/synthesis/ScaleWeight.scala @@ -0,0 +1,12 @@ +import leon.Utils._ + +object ScaleWeight { + + def sw(weight: Int): (Int, Int, Int, Int) = choose((w4:Int,w3:Int,w2:Int,w1:Int) => ( + w1 + 3 * w2 + 9 * w3 + 27 * w4 == weight + && -1 <= w1 && w1 <= 1 + && -1 <= w2 && w2 <= 1 + && -1 <= w3 && w3 <= 1 + && -1 <= w4 && w4 <= 1 + )) +}