diff options
Diffstat (limited to 'test/regress/regress0/sygus/let-ringer.sy')
| -rw-r--r-- | test/regress/regress0/sygus/let-ringer.sy | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/test/regress/regress0/sygus/let-ringer.sy b/test/regress/regress0/sygus/let-ringer.sy index 0fe8dd05e..c02d2b31f 100644 --- a/test/regress/regress0/sygus/let-ringer.sy +++ b/test/regress/regress0/sygus/let-ringer.sy @@ -3,12 +3,14 @@ ; COMMAND-LINE: --cegqi-si=all --sygus-unif --sygus-out=status (set-logic LIA) (define-fun g ((x Int)) Int (ite (= x 1) 15 19)) +(define-fun letf ((z Int) (w Int) (s Int) (x Int)) Int (+ z (+ x (+ x (+ s (+ 1 (+ (g w) z))))))) + (synth-fun f ((x Int)) Int ((Start Int (x 0 1 (- Start Start) - (let ((z Int Start) (w Int Start)) (+ z (+ x (+ x (+ Start (+ 1 (+ (g w) z))))))))))) + (letf Start Start Start x))))) (declare-var x Int) (constraint (= (f x) (+ (* 4 x) 15))) |