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