diff options
Diffstat (limited to 'test/regress/regress1/quantifiers/parametric-lists.smt2')
| -rw-r--r-- | test/regress/regress1/quantifiers/parametric-lists.smt2 | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/test/regress/regress1/quantifiers/parametric-lists.smt2 b/test/regress/regress1/quantifiers/parametric-lists.smt2 index c45152d6f..f236c1ec7 100644 --- a/test/regress/regress1/quantifiers/parametric-lists.smt2 +++ b/test/regress/regress1/quantifiers/parametric-lists.smt2 @@ -1,9 +1,8 @@ -; COMMAND-LINE: --lang=smt2.5 ; EXPECT: unsat (set-logic ALL_SUPPORTED) (set-info :status unsat) -(declare-datatypes (T) ((List (cons (head T) (tail (List T))) (nil)))) -(declare-datatypes () ((KV (kv (key Int) (value Int)) (nilKV)))) ; key value pair +(declare-datatypes ((List 1)) ((par (T) ((cons (head T) (tail (List T))) (nil))))) +(declare-datatypes ((KV 0)) (((kv (key Int) (value Int)) (nilKV)))) (declare-fun mapper ((List Int)) (List KV)) (assert (forall @@ -13,7 +12,7 @@ (= (as nil (List KV)) (mapper input)) (= (cons (kv 0 (head input)) (mapper (tail input))) (mapper input)) ) - ) + ) ) (declare-fun reduce ((List KV)) Int) (assert @@ -41,4 +40,3 @@ (not (= (sum (cons 0 (as nil (List Int)))) (reduce (mapper (cons 0 (as nil (List Int))))))) ) (check-sat) - |