Skip to content

Corrected reversed inputs and outputs in Messy benchmarks. #26

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
Shoooooon wants to merge 4 commits into
base: main
Choose a base branch
from
Open

Corrected reversed inputs and outputs in Messy benchmarks. #26

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
9d8a9ca
Corrected reversed inputs and outputs in Messy benchmarks.
Shoooooon Mar 1, 2024
3961b39
Fixed 2 typos in benchmarks.
Shoooooon Mar 1, 2024
3693fc8
Removed inverted messy benchmarks files.
Shoooooon Mar 1, 2024
2e557f3
Removed inaccurate readme.
Shoooooon Mar 2, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion benchmarks/messy/basic_bv/BVtest_ADD_01.sem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,6 @@
(synth-fun BVtest_ADD_01() Start)


(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_ADD_01 #x00000004 #x00000004 #x00000003 y)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_ADD_01 #x00000003 y #x00000004 #x00000004)))

(check-synth)
4 changes: 2 additions & 2 deletions benchmarks/messy/basic_bv/BVtest_AND_01.sem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@
(synth-fun BVtest_AND_01() Start)


(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_AND_01 #x00000009 #x00000006 #x00000000 y)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_AND_01 #x000000f7 #x0000002c #x00000024 y)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_AND_01 #x00000000 y #x00000009 #x00000006)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_AND_01 #x00000024 y #x000000f7 #x0000002c)))

(check-synth)
4 changes: 2 additions & 2 deletions benchmarks/messy/basic_bv/BVtest_AND_02.sem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@
(synth-fun BVtest_AND_02() Start)


(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_AND_02 #x00000009 #x00000006 #x00000000 y)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_AND_02 #x000000f7 #x0000002c #x00000024 y)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_AND_02 #x00000000 y #x00000009 #x00000006)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_AND_02 #x00000024 y #x000000f7 #x0000002c)))

(check-synth)
4 changes: 2 additions & 2 deletions benchmarks/messy/basic_bv/BVtest_AND_03.sem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@
(synth-fun BVtest_AND_03() Start)


(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_AND_03 #x00000009 #x00000006 #x00000000 y)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_AND_03 #x000000f7 #x0000002c #x00000024 y)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_AND_03 #x00000000 y #x00000009 #x00000006)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_AND_03 #x00000024 y #x000000f7 #x0000002c)))

(check-synth)
8 changes: 4 additions & 4 deletions benchmarks/messy/basic_bv/BVtest_MAX_01.sem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,9 +35,9 @@
(synth-fun BVtest_MAX_01() Start)


(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_MAX_01 #x00000009 #x00000006 #x00000009 y)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_MAX_01 #x0000002c #x000000f7 #x000000f7 y)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_MAX_01 #x00000020 #x00000011 #x00000020 y)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_MAX_01 #x0000008e #x0000008e #x0000008e y)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_MAX_01 #x00000009 y #x00000009 #x00000006)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_MAX_01 #x000000f7 y #x0000002c #x000000f7)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_MAX_01 #x00000020 y #x00000020 #x00000011)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_MAX_01 #x0000008e y #x0000008e #x0000008e)))

(check-synth)
4 changes: 2 additions & 2 deletions benchmarks/messy/basic_bv/BVtest_NAND_01.sem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@
(synth-fun BVtest_NAND_01() Start)


(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_NAND_01 #x00000009 #x00000006 #x0000001f y)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_NAND_01 #x000000f7 #x0000002c #x000000d1 y)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_NAND_01 #x0000001f y #x00000009 #x00000006)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_NAND_01 #x000000d1 y #x000000f7 #x0000002c)))

(check-synth)
4 changes: 2 additions & 2 deletions benchmarks/messy/basic_bv/BVtest_PLUS_01.sem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@
(synth-fun BVtest_PLUS_01() Start)


(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_PLUS_01 #x00000009 #x00000006 #x0000000f y)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_PLUS_01 #x000000f7 #x0000002c #x00000123 y)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_PLUS_01 #x0000000f y #x00000009 #x00000006)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_PLUS_01 #x00000123 y #x000000f7 #x0000002c)))

(check-synth)
4 changes: 2 additions & 2 deletions benchmarks/messy/basic_bv/BVtest_Swap_XOR_01.sem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@
(synth-fun BVtest_Swap_XOR_01() Start)


(constraint (Start.Sem BVtest_Swap_XOR_01 #x00000009 #x00000006 #x00000006 #x00000009))
(constraint (Start.Sem BVtest_Swap_XOR_01 #x000000f7 #x0000002c #x0000002c #x000000f7))
(constraint (Start.Sem BVtest_Swap_XOR_01 #x00000006 #x00000009 #x00000009 #x00000006))
(constraint (Start.Sem BVtest_Swap_XOR_01 #x0000002c #x000000f7 #x000000f7 #x0000002c))

(check-synth)
4 changes: 2 additions & 2 deletions benchmarks/messy/basic_bv/BVtest_Swap_XOR_02.sem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@
(synth-fun BVtest_Swap_XOR_02() Start)


(constraint (Start.Sem BVtest_Swap_XOR_02 #x00000009 #x00000006 #x00000006 #x00000009))
(constraint (Start.Sem BVtest_Swap_XOR_02 #x000000f7 #x0000002c #x0000002c #x000000f7))
(constraint (Start.Sem BVtest_Swap_XOR_02 #x00000006 #x00000009 #x00000009 #x00000006))
(constraint (Start.Sem BVtest_Swap_XOR_02 #x0000002c #x000000f7 #x000000f7 #x0000002c))

(check-synth)
4 changes: 2 additions & 2 deletions benchmarks/messy/basic_bv/BVtest_Swap_XOR_03.sem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@
(synth-fun BVtest_Swap_XOR_03() Start)


(constraint (Start.Sem BVtest_Swap_XOR_03 #x00000009 #x00000006 #x00000006 #x00000009))
(constraint (Start.Sem BVtest_Swap_XOR_03 #x000000f7 #x0000002c #x0000002c #x000000f7))
(constraint (Start.Sem BVtest_Swap_XOR_03 #x00000006 #x00000009 #x00000009 #x00000006))
(constraint (Start.Sem BVtest_Swap_XOR_03 #x0000002c #x000000f7 #x000000f7 #x0000002c))

(check-synth)
6 changes: 3 additions & 3 deletions benchmarks/messy/basic_bv/BVtest_While_01_XOR_by_AND_OR.sem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,8 +55,8 @@
(synth-fun BVtest_While_01_XOR_by_AND_OR() Start)


(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_While_01_XOR_by_AND_OR #x00000006 #x00000009 #x0000000f y)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_While_01_XOR_by_AND_OR #x000000f7 #x0000002c #x000000db y)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_While_01_XOR_by_AND_OR #x0000000e #x0000000f #x00000001 y)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_While_01_XOR_by_AND_OR #x0000000f y #x00000006 #x00000009)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_While_01_XOR_by_AND_OR #x000000db y #x000000f7 #x0000002c)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_While_01_XOR_by_AND_OR #x00000001 y #x0000000e #x0000000f)))

(check-synth)
6 changes: 3 additions & 3 deletions benchmarks/messy/basic_bv/BVtest_While_02_XOR_by_AND_OR_ADD.sem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,8 +55,8 @@
(synth-fun BVtest_While_02_XOR_by_AND_OR_ADD() Start)


(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_While_02_XOR_by_AND_OR_ADD #x00000009 #x00000006 #x0000000f y)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_While_02_XOR_by_AND_OR_ADD #x000000f7 #x0000002c #x000000db y)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_While_02_XOR_by_AND_OR_ADD #x0000000e #x0000000f #x00000001 y)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_While_02_XOR_by_AND_OR_ADD #x0000000f y #x00000009 #x00000006)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_While_02_XOR_by_AND_OR_ADD #x000000db y #x000000f7 #x0000002c)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_While_02_XOR_by_AND_OR_ADD #x00000001 y #x0000000e #x0000000f)))

(check-synth)
4 changes: 2 additions & 2 deletions benchmarks/messy/basic_bv/BVtest_XOR_01.sem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,7 @@
(synth-fun BVtest_XOR_01() Start)


(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_XOR_01 #x00000009 #x00000006 #x0000000f y)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_XOR_01 #x000000f7 #x0000002c #x000000db y)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_XOR_01 #x0000000f y #x00000009 #x00000006)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_XOR_01 #x000000db y #x000000f7 #x0000002c)))

(check-synth)
4 changes: 2 additions & 2 deletions benchmarks/messy/basic_bv/BVtest_XOR_02.sem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@
(synth-fun BVtest_XOR_02() Start)


(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_XOR_02 #x00000009 #x00000006 #x0000000f y)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_XOR_02 #x000000f7 #x0000002c #x000000db y)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_XOR_02 #x0000000f y #x00000009 #x00000006)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_XOR_02 #x000000db y #x000000f7 #x0000002c)))

(check-synth)
6 changes: 3 additions & 3 deletions benchmarks/messy/basic_bv/BVtest_XOR_03.sem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,8 +35,8 @@
(synth-fun BVtest_XOR_03() Start)


(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_XOR_03 #x00000009 #x00000006 #x0000000f y)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_XOR_03 #x000000f7 #x0000002c #x000000db y)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_XOR_03 #x0000000e #x0000000f #x00000001 y)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_XOR_03 #x0000000f y #x00000009 #x00000006)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_XOR_03 #x000000db y #x000000f7 #x0000002c)))
(constraint (exists ((y (_ BitVec 32))) (Start.Sem BVtest_XOR_03 #x00000001 y #x0000000e #x0000000f)))

(check-synth)
4 changes: 2 additions & 2 deletions benchmarks/messy/basic_impv/basicTest_AddByWhileLoop_01.sem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,7 @@
(synth-fun basicTest_AddByWhileLoop_01() Start)


(constraint (Start.Sem basicTest_AddByWhileLoop_01 4 10 10 10))
(constraint (Start.Sem basicTest_AddByWhileLoop_01 12 20 20 20))
(constraint (Start.Sem basicTest_AddByWhileLoop_01 10 10 4 10))
(constraint (Start.Sem basicTest_AddByWhileLoop_01 20 20 12 20))

(check-synth)
6 changes: 3 additions & 3 deletions benchmarks/messy/basic_impv/basicTest_AddByWhileLoop_02.sem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,8 +51,8 @@
(synth-fun basicTest_AddByWhileLoop_02() Start)


(constraint (Start.Sem basicTest_AddByWhileLoop_02 4 10 10 10))
(constraint (Start.Sem basicTest_AddByWhileLoop_02 12 20 20 20))
(constraint (Start.Sem basicTest_AddByWhileLoop_02 20 12 12 12))
(constraint (Start.Sem basicTest_AddByWhileLoop_02 10 10 4 10))
(constraint (Start.Sem basicTest_AddByWhileLoop_02 20 20 12 20))
(constraint (Start.Sem basicTest_AddByWhileLoop_02 12 12 20 12))

(check-synth)
6 changes: 3 additions & 3 deletions benchmarks/messy/basic_impv/basicTest_AddByWhileLoop_03.sem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,8 +44,8 @@
(synth-fun basicTest_AddByWhileLoop_03() Start)


(constraint (Start.Sem basicTest_AddByWhileLoop_03 4 10 10 10))
(constraint (Start.Sem basicTest_AddByWhileLoop_03 12 20 20 20))
(constraint (Start.Sem basicTest_AddByWhileLoop_03 20 12 12 12))
(constraint (Start.Sem basicTest_AddByWhileLoop_03 10 10 4 10))
(constraint (Start.Sem basicTest_AddByWhileLoop_03 20 20 12 20))
(constraint (Start.Sem basicTest_AddByWhileLoop_03 12 12 20 12))

(check-synth)
6 changes: 3 additions & 3 deletions benchmarks/messy/basic_impv/basicTest_AddByWhileLoop_04.sem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -58,8 +58,8 @@
(synth-fun basicTest_AddByWhileLoop_04() Start)


(constraint (Start.Sem basicTest_AddByWhileLoop_04 4 10 10 10))
(constraint (Start.Sem basicTest_AddByWhileLoop_04 12 20 20 20))
(constraint (Start.Sem basicTest_AddByWhileLoop_04 20 12 12 12))
(constraint (Start.Sem basicTest_AddByWhileLoop_04 10 10 4 10))
(constraint (Start.Sem basicTest_AddByWhileLoop_04 20 20 12 20))
(constraint (Start.Sem basicTest_AddByWhileLoop_04 12 12 20 12))

(check-synth)
6 changes: 3 additions & 3 deletions benchmarks/messy/basic_impv/basicTest_AddByWhileLoop_05.sem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,8 +61,8 @@
(synth-fun basicTest_AddByWhileLoop_05() Start)


(constraint (Start.Sem basicTest_AddByWhileLoop_05 4 10 10 10))
(constraint (Start.Sem basicTest_AddByWhileLoop_05 12 20 20 20))
(constraint (Start.Sem basicTest_AddByWhileLoop_05 20 12 12 12))
(constraint (Start.Sem basicTest_AddByWhileLoop_05 10 10 4 10))
(constraint (Start.Sem basicTest_AddByWhileLoop_05 20 20 12 20))
(constraint (Start.Sem basicTest_AddByWhileLoop_05 12 12 20 12))

(check-synth)
8 changes: 4 additions & 4 deletions benchmarks/messy/basic_impv/basicTest_AddOne_01.sem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,9 +26,9 @@
(synth-fun basicTest_AddOne_01() Start)


(constraint (Start.Sem basicTest_AddOne_01 4 5))
(constraint (Start.Sem basicTest_AddOne_01 2 3))
(constraint (Start.Sem basicTest_AddOne_01 1 2))
(constraint (Start.Sem basicTest_AddOne_01 8 9))
(constraint (Start.Sem basicTest_AddOne_01 5 4))
(constraint (Start.Sem basicTest_AddOne_01 3 2))
(constraint (Start.Sem basicTest_AddOne_01 2 1))
(constraint (Start.Sem basicTest_AddOne_01 9 8))

(check-synth)
6 changes: 3 additions & 3 deletions benchmarks/messy/basic_impv/basicTest_Fib_01.sem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -66,8 +66,8 @@
(synth-fun basicTest_Fib_01() Start)


(constraint (exists ((i Int) (y Int)) (Start.Sem basicTest_Fib_01 1 1 1 1 y i)))
(constraint (exists ((i Int) (y Int)) (Start.Sem basicTest_Fib_01 1 1 5 5 y i)))
(constraint (exists ((i Int) (y Int)) (Start.Sem basicTest_Fib_01 1 1 10 55 y i)))
(constraint (exists ((i Int) (y Int)) (Start.Sem basicTest_Fib_01 1 y i 1 1 1)))
(constraint (exists ((i Int) (y Int)) (Start.Sem basicTest_Fib_01 5 y i 1 1 5)))
(constraint (exists ((i Int) (y Int)) (Start.Sem basicTest_Fib_01 55 y i 1 1 10)))

(check-synth)
2 changes: 1 addition & 1 deletion benchmarks/messy/basic_impv/basicTest_MAX_01.sem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,7 @@


(constraint (Start.Sem basicTest_MAX_01 4 1 4 1))
(constraint (Start.Sem basicTest_MAX_01 2 6 6 2))
(constraint (Start.Sem basicTest_MAX_01 6 2 2 6))
(constraint (Start.Sem basicTest_MAX_01 1 1 1 1))
(constraint (Start.Sem basicTest_MAX_01 8 8 8 8))

Expand Down
2 changes: 1 addition & 1 deletion benchmarks/messy/basic_impv/basicTest_MAX_02.sem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@


(constraint (Start.Sem basicTest_MAX_02 4 1 4 1))
(constraint (Start.Sem basicTest_MAX_02 2 6 6 2))
(constraint (Start.Sem basicTest_MAX_02 6 2 2 6))
(constraint (Start.Sem basicTest_MAX_02 1 1 1 1))
(constraint (Start.Sem basicTest_MAX_02 8 8 8 8))

Expand Down
8 changes: 4 additions & 4 deletions benchmarks/messy/basic_impv/basicTest_MAX_03.sem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,9 +51,9 @@
(synth-fun basicTest_MAX_03() Start)


(constraint (exists ((c Int)) (Start.Sem basicTest_MAX_03 4 1 4123 4 1 c)))
(constraint (exists ((c Int)) (Start.Sem basicTest_MAX_03 2 6 4123 6 2 c)))
(constraint (exists ((c Int)) (Start.Sem basicTest_MAX_03 1 1 4123 1 1 c)))
(constraint (exists ((c Int)) (Start.Sem basicTest_MAX_03 8 8 4123 8 8 c)))
(constraint (exists ((c Int)) (Start.Sem basicTest_MAX_03 4 1 c 4 1 4123)))
(constraint (exists ((c Int)) (Start.Sem basicTest_MAX_03 6 2 c 2 6 4123)))
(constraint (exists ((c Int)) (Start.Sem basicTest_MAX_03 1 1 c 1 1 4123)))
(constraint (exists ((c Int)) (Start.Sem basicTest_MAX_03 8 8 c 8 8 4123)))

(check-synth)
6 changes: 3 additions & 3 deletions benchmarks/messy/basic_impv/basicTest_MultByWhileLoop_01.sem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -124,8 +124,8 @@
(synth-fun basicTest_MultByWhileLoop_01() Start)


(constraint (exists ((y Int) (i Int) (j Int) (x Int)) (Start.Sem basicTest_MultByWhileLoop_01 4 0 0 10 0 x j i y 40)))
(constraint (exists ((y Int) (i Int) (j Int) (x Int)) (Start.Sem basicTest_MultByWhileLoop_01 5 0 0 6 0 x j i y 30)))
(constraint (exists ((y Int) (i Int) (j Int) (x Int)) (Start.Sem basicTest_MultByWhileLoop_01 8 0 0 3 0 x j i y 24)))
(constraint (exists ((y Int) (i Int) (j Int) (x Int)) (Start.Sem basicTest_MultByWhileLoop_01 x j i y 40 4 0 0 10 0)))
(constraint (exists ((y Int) (i Int) (j Int) (x Int)) (Start.Sem basicTest_MultByWhileLoop_01 x j i y 30 5 0 0 6 0)))
(constraint (exists ((y Int) (i Int) (j Int) (x Int)) (Start.Sem basicTest_MultByWhileLoop_01 x j i y 24 8 0 0 3 0)))

(check-synth)
6 changes: 3 additions & 3 deletions benchmarks/messy/basic_impv/basicTest_MultByWhileLoop_02.sem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,8 +75,8 @@
(synth-fun basicTest_MultByWhileLoop_02() Start)


(constraint (exists ((y Int) (x Int)) (Start.Sem basicTest_MultByWhileLoop_02 4 10 0 x y 40)))
(constraint (exists ((y Int) (x Int)) (Start.Sem basicTest_MultByWhileLoop_02 5 6 0 x y 30)))
(constraint (exists ((y Int) (x Int)) (Start.Sem basicTest_MultByWhileLoop_02 8 3 0 x y 24)))
(constraint (exists ((y Int) (x Int)) (Start.Sem basicTest_MultByWhileLoop_02 x y 40 4 10 0)))
(constraint (exists ((y Int) (x Int)) (Start.Sem basicTest_MultByWhileLoop_02 x y 30 5 6 0)))
(constraint (exists ((y Int) (x Int)) (Start.Sem basicTest_MultByWhileLoop_02 x y 24 8 3 0)))

(check-synth)
2 changes: 1 addition & 1 deletion benchmarks/messy/basic_impv/basicTest_Sanity01.sem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -70,6 +70,6 @@
(synth-fun basicTest_Sanity01() Start)


(constraint (Start.Sem basicTest_Sanity01 4 10))
(constraint (Start.Sem basicTest_Sanity01 10 4))

(check-synth)
6 changes: 3 additions & 3 deletions benchmarks/messy/basic_impv/basicTest_SetBothtoLarger_01.sem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,8 +53,8 @@
(synth-fun basicTest_SetBothtoLarger_01() Start)


(constraint (Start.Sem basicTest_SetBothtoLarger_01 4 10 10 10))
(constraint (Start.Sem basicTest_SetBothtoLarger_01 12 20 20 20))
(constraint (Start.Sem basicTest_SetBothtoLarger_01 20 12 20 20))
(constraint (Start.Sem basicTest_SetBothtoLarger_01 10 10 4 10))
(constraint (Start.Sem basicTest_SetBothtoLarger_01 20 20 12 20))
(constraint (Start.Sem basicTest_SetBothtoLarger_01 20 20 20 12))

(check-synth)
4 changes: 2 additions & 2 deletions benchmarks/messy/basic_impv/basicTest_SumByWhileLoop_01.sem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,7 @@
(synth-fun basicTest_SumByWhileLoop_01() Start)


(constraint (exists ((v Int) (y Int) (z Int) (w Int)) (Start.Sem basicTest_SumByWhileLoop_01 2 5 4 3 1 w z y 15 v)))
(constraint (exists ((v Int) (y Int) (z Int) (w Int)) (Start.Sem basicTest_SumByWhileLoop_01 21 16 13 11 9 w z y 70 v)))
(constraint (exists ((v Int) (y Int) (z Int) (w Int)) (Start.Sem basicTest_SumByWhileLoop_01 w z y 15 v 2 5 4 3 1)))
(constraint (exists ((v Int) (y Int) (z Int) (w Int)) (Start.Sem basicTest_SumByWhileLoop_01 w z y 70 v 21 16 13 11 9)))

(check-synth)
4 changes: 2 additions & 2 deletions benchmarks/messy/basic_impv/basicTest_SumWithLimitedOps_01.sem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@
(synth-fun basicTest_SumWithLimitedOps_01() Start)


(constraint (exists ((v Int) (y Int) (z Int) (w Int)) (Start.Sem basicTest_SumWithLimitedOps_01 2 5 4 3 1 w z y 15 v)))
(constraint (exists ((v Int) (y Int) (z Int) (w Int)) (Start.Sem basicTest_SumWithLimitedOps_01 21 16 13 11 9 w z y 70 v)))
(constraint (exists ((v Int) (y Int) (z Int) (w Int)) (Start.Sem basicTest_SumWithLimitedOps_01 w z y 15 v 2 5 4 3 1)))
(constraint (exists ((v Int) (y Int) (z Int) (w Int)) (Start.Sem basicTest_SumWithLimitedOps_01 w z y 70 v 21 16 13 11 9)))

(check-synth)
4 changes: 2 additions & 2 deletions benchmarks/messy/basic_impv/basicTest_SumWithLimitedOps_02.sem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@
(synth-fun basicTest_SumWithLimitedOps_02() Start)


(constraint (exists ((v Int) (y Int) (z Int) (w Int)) (Start.Sem basicTest_SumWithLimitedOps_02 2 5 4 3 1 w z y 15 v)))
(constraint (exists ((v Int) (y Int) (z Int) (w Int)) (Start.Sem basicTest_SumWithLimitedOps_02 21 16 13 11 9 w z y 70 v)))
(constraint (exists ((v Int) (y Int) (z Int) (w Int)) (Start.Sem basicTest_SumWithLimitedOps_02 w z y 15 v 2 5 4 3 1)))
(constraint (exists ((v Int) (y Int) (z Int) (w Int)) (Start.Sem basicTest_SumWithLimitedOps_02 w z y 70 v 21 16 13 11 9)))

(check-synth)
2 changes: 1 addition & 1 deletion benchmarks/messy/basic_impv/minimal_unsat.sem
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -73,6 +73,6 @@
(synth-fun minimal_unsat() Start)


(constraint (exists ((n Int)) (Start.Sem minimal_unsat 5 4 2 n)))
(constraint (exists ((n Int)) (Start.Sem minimal_unsat 2 n 5 4)))

(check-synth)
Loading