From cc3181896d2cdef1f96a9880921660c9a4144757 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com> Date: Thu, 29 Nov 2012 16:15:06 +0100 Subject: [PATCH] new testcase --- testcases/synthesis/ScaleWeight.scala | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 testcases/synthesis/ScaleWeight.scala diff --git a/testcases/synthesis/ScaleWeight.scala b/testcases/synthesis/ScaleWeight.scala new file mode 100644 index 000000000..7e1c0f2ea --- /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 + )) +} -- GitLab