diff options
| author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2020-03-28 14:31:37 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-28 14:31:37 -0500 |
| commit | a7f4f4fcf4d42f2c5b60bd62d3fd914f31202f64 (patch) | |
| tree | eec8ff7d01a9465f2e3220cab41517053ba8f750 /test/regress | |
| parent | 830c09d3cadc119845aff27684bd68c16e442692 (diff) | |
Change is-cons to (_ is cons) in Sygus benchmarks. (#4174)
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/regress1/sygus/dt-test-ns.sy | 4 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/list-head-x.sy | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/test/regress/regress1/sygus/dt-test-ns.sy b/test/regress/regress1/sygus/dt-test-ns.sy index 3d078cc25..90fa57827 100644 --- a/test/regress/regress1/sygus/dt-test-ns.sy +++ b/test/regress/regress1/sygus/dt-test-ns.sy @@ -1,6 +1,6 @@ ; EXPECT: unsat ; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status -(set-logic LIA) +(set-logic DTLIA) (declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil)))) @@ -8,6 +8,6 @@ (declare-var x Int) -(constraint (is-cons (f x))) +(constraint ((_ is cons) (f x))) (constraint (and (= (head (f x)) x) (= (head (f x)) (+ 5 (head (tail (f x))))))) (check-synth) diff --git a/test/regress/regress1/sygus/list-head-x.sy b/test/regress/regress1/sygus/list-head-x.sy index 83ac8290d..ae2bcc00e 100644 --- a/test/regress/regress1/sygus/list-head-x.sy +++ b/test/regress/regress1/sygus/list-head-x.sy @@ -8,6 +8,6 @@ (declare-var x Int) -(constraint (is-cons (f x))) +(constraint ((_ is cons) (f x))) (constraint (= (head (f x)) (+ x 7))) (check-synth) |