diff options
Diffstat (limited to 'test/regress/regress1/sygus/issue3461.sy')
| -rw-r--r-- | test/regress/regress1/sygus/issue3461.sy | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/test/regress/regress1/sygus/issue3461.sy b/test/regress/regress1/sygus/issue3461.sy index 1f839c229..08b5738c1 100644 --- a/test/regress/regress1/sygus/issue3461.sy +++ b/test/regress/regress1/sygus/issue3461.sy @@ -1,15 +1,16 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic ALL_SUPPORTED) (declare-datatype Doc ((D (owner Int) (body Int)))) -(declare-datatype Policy - ((p (principal Int)) +(declare-datatype Policy + ((p (principal Int)) (por (left Policy) (right Policy)))) (synth-fun mkPolicy ((d Doc)) Policy + ((Start Policy) (Q Policy)) ((Start Policy (Q)) (Q Policy ((p 0) (p 1) (por Q Q)))) ) |