diff --git a/test/regress/cli/regress0/quantifiers/dd_spark2014-pat.smt2 b/test/regress/cli/regress0/quantifiers/dd_spark2014-pat.smt2 index 9168a5d1c2a..babf76bbbba 100644 --- a/test/regress/cli/regress0/quantifiers/dd_spark2014-pat.smt2 +++ b/test/regress/cli/regress0/quantifiers/dd_spark2014-pat.smt2 @@ -1,15 +1,15 @@ ; EXPECT: unsat (set-logic ALL) (declare-sort i 0) -(declare-fun i (i) Int) -(define-fun t ((x i)) Int (i x)) +(declare-fun ii (i) Int) +(define-fun t ((x i)) Int (ii x)) (declare-fun o (Int) i) (assert (forall ((x i)) (! (= x (o (t x))) :pattern ((t x))))) (declare-sort t 0) (declare-fun l (t) i) (declare-fun m (Int Int) t) -(declare-datatypes ((u 0)) (((u (e (Array Int i)) (r t))))) +(declare-datatypes ((u 0)) (((uc (e (Array Int i)) (r t))))) (declare-fun s (i Int) (Array Int i)) (assert (forall ((v i)) (forall ((i Int)) (= v (select (s v i) i))))) -(assert (exists ((n u)) (not (=> (exists ((o i)) (= 1 (i o))) (= (- 1) (i (l (r (u (s (o 1) 0) (m 0 0)))))) (= 1 (i (select (e (u (s (o 1) (- 1)) (m 0 0))) (i (l (r (u (s (o 1) 0) (m 0 0)))))))))))) +(assert (exists ((n u)) (not (=> (exists ((o i)) (= 1 (ii o))) (= (- 1) (ii (l (r (uc (s (o 1) 0) (m 0 0)))))) (= 1 (ii (select (e (uc (s (o 1) (- 1)) (m 0 0))) (ii (l (r (uc (s (o 1) 0) (m 0 0)))))))))))) (check-sat)