diff options
Diffstat (limited to 'test/regress/regress0/sygus/let-simp.sy')
| -rw-r--r-- | test/regress/regress0/sygus/let-simp.sy | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/test/regress/regress0/sygus/let-simp.sy b/test/regress/regress0/sygus/let-simp.sy index 6f9d9fff9..7e191e312 100644 --- a/test/regress/regress0/sygus/let-simp.sy +++ b/test/regress/regress0/sygus/let-simp.sy @@ -1,12 +1,13 @@ ; EXPECT: unsat ; COMMAND-LINE: --cegqi-si=all --sygus-out=status (set-logic LIA) +(define-fun letf ((z Int)) Int (+ z z)) (synth-fun f ((x Int) (y Int)) Int ((Start Int (x y 0 (- Start Start) - (let ((z Int Start)) (+ z z)))))) + (letf Start))))) (declare-var x Int) (declare-var y Int) |