diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-21 19:38:40 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-08-21 19:38:40 -0500 |
| commit | ab8d44b83e210ed38623a1440e3ef1d318f7d0d0 (patch) | |
| tree | b241f69ddf7715eb1bfe0753e59ed02a12507da3 /test/regress/regress1/sygus/let-bug-simp.sy | |
| parent | 5b655946e1c73f511719d0264f92715b063e867f (diff) | |
Fix processing of nested Variable construct in sygus let bodies (#2351)
Diffstat (limited to 'test/regress/regress1/sygus/let-bug-simp.sy')
| -rw-r--r-- | test/regress/regress1/sygus/let-bug-simp.sy | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/let-bug-simp.sy b/test/regress/regress1/sygus/let-bug-simp.sy new file mode 100644 index 000000000..d570d5a21 --- /dev/null +++ b/test/regress/regress1/sygus/let-bug-simp.sy @@ -0,0 +1,22 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic LIA) + +(synth-fun f ((x0 Int) (x1 Int)) Bool +( + (StartInt Int (5)) + + (Start Bool ( + (let + ((z Int StartInt)) + (or + (= (Variable Int) z) + (= (Variable Int) z))))) +) +) + +(declare-var a Int) +(declare-var b Int) +(constraint (=> (= a 5) (f a b))) +(constraint (=> (= b 5) (f a b))) +(check-synth) |