diff options
Diffstat (limited to 'test/regress/regress0/sygus/clock-inc-tuple.sy')
-rw-r--r-- | test/regress/regress0/sygus/clock-inc-tuple.sy | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/test/regress/regress0/sygus/clock-inc-tuple.sy b/test/regress/regress0/sygus/clock-inc-tuple.sy new file mode 100644 index 000000000..09bdb8b4d --- /dev/null +++ b/test/regress/regress0/sygus/clock-inc-tuple.sy @@ -0,0 +1,14 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si --no-dump-synth + +(set-logic ALL_SUPPORTED) +(declare-var m Int) +(declare-var s Int) +(declare-var inc Int) +(declare-datatypes () ( (tuple2 (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) |