diff options
Diffstat (limited to 'test/regress/regress1/sygus/issue3580.sy')
-rw-r--r-- | test/regress/regress1/sygus/issue3580.sy | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/issue3580.sy b/test/regress/regress1/sygus/issue3580.sy new file mode 100644 index 000000000..9da07407a --- /dev/null +++ b/test/regress/regress1/sygus/issue3580.sy @@ -0,0 +1,24 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status --sygus-active-gen=none --lang=sygus2 +(set-logic ALL) +(synth-fun f + () Bool + ((B Bool)) + ( + (B Bool (true)) + ) +) +(synth-fun g + ((r Int)) Bool + ((B Bool) (I Int) (IConst Int)) + ( + (B Bool ((= I I) (=> B B))) + (I Int (r 0 (mod I IConst))) + (IConst Int ((Constant Int))) + ) +) +(constraint (g 0)) +(constraint (not (g 1))) +(constraint (g 2)) +(constraint f) +(check-synth) |