Fix

ajreynol · Dec 17, 2024 · f6244cd · f6244cd
1 parent 219a7ab
commit f6244cd
Showing 1 changed file with 4 additions and 4 deletions.
diff --git 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)