diff options
Diffstat (limited to 'test/regress/regress1/sygus/double.sy')
-rw-r--r-- | test/regress/regress1/sygus/double.sy | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/double.sy b/test/regress/regress1/sygus/double.sy new file mode 100644 index 000000000..f3fea3122 --- /dev/null +++ b/test/regress/regress1/sygus/double.sy @@ -0,0 +1,26 @@ +; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+
+(set-logic SLIA)
+(declare-datatype Ex ((Ex2 (ex Int))))
+
+(synth-fun double ((x1 Ex)) Int
+ (
+ (Start Int (ntInt))
+ (ntInt Int
+ (
+ (ex ntEx)
+ (+ ntInt ntInt)
+ )
+ )
+ (ntEx Ex
+ (
+ x1
+ (Ex2 ntInt)
+ )
+ )
+ )
+)
+(constraint (= (double (Ex2 1)) 2))
+(constraint (= (double (Ex2 4)) 8))
+(check-synth)
|