diff options
Diffstat (limited to 'test/regress/regress1/sygus/commutative-stream.sy')
-rw-r--r-- | test/regress/regress1/sygus/commutative-stream.sy | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/commutative-stream.sy b/test/regress/regress1/sygus/commutative-stream.sy new file mode 100644 index 000000000..b07051d37 --- /dev/null +++ b/test/regress/regress1/sygus/commutative-stream.sy @@ -0,0 +1,24 @@ +; EXPECT: (define-fun comm ((x Int) (y Int)) Int (+ x y)) +; EXPECT: (define-fun comm ((x Int) (y Int)) Int (- x x)) +; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded. +; EXPECT: ") +; EXIT: 1 + +; COMMAND-LINE: --sygus-stream --sygus-abort-size=2 + +(set-logic LIA) + +(synth-fun comm ((x Int) (y Int)) Int + ((Start Int (x + y + (+ Start Start) + (- Start Start) + )) + )) + +(declare-var x Int) +(declare-var y Int) + +(constraint (= (comm x y) (comm y x))) + +(check-synth) |