diff options
Diffstat (limited to 'test/regress/regress1/sygus/clock-inc-tuple.sy')
| -rw-r--r-- | test/regress/regress1/sygus/clock-inc-tuple.sy | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/clock-inc-tuple.sy b/test/regress/regress1/sygus/clock-inc-tuple.sy new file mode 100644 index 000000000..43fd7c1ac --- /dev/null +++ b/test/regress/regress1/sygus/clock-inc-tuple.sy @@ -0,0 +1,14 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si=all --sygus-out=status + +(set-logic ALL_SUPPORTED) +(declare-var m Int) +(declare-var s Int) +(declare-var inc Int) +(declare-datatypes ((tuple2 0)) ( ((tuple2 (_m Int) (_s Int))) )) + +(synth-fun x12 ((m Int) (s Int) (inc Int)) tuple2) +(constraint (=> +(and (>= m 0) (>= s 0) (< s 3) (> inc 0)) +(and (>= (_m (x12 m s inc)) 0) (>= (_s (x12 m s inc)) 0) (< (_s (x12 m s inc)) 3) (= (+ (* (_m (x12 m s inc)) 3) (_s (x12 m s inc))) (+ (+ (* m 3) s) inc))))) +(check-synth) |