diff --git a/tests/sat/test-007.smt2 b/tests/sat/test-007.smt2 index 62c9e167..ba7c3048 100644 --- a/tests/sat/test-007.smt2 +++ b/tests/sat/test-007.smt2 @@ -1,2 +1,6 @@ +(declare-sort $i 0) +(declare-fun a () $i) +(declare-fun b () $i) +(declare-fun c () $i) (assert (and (= a b) (= b c))) (check-sat) diff --git a/tests/sat/test-010.smt2 b/tests/sat/test-010.smt2 index dbec8ea3..5a2149b3 100644 --- a/tests/sat/test-010.smt2 +++ b/tests/sat/test-010.smt2 @@ -1,2 +1,7 @@ +(declare-sort $i 0) +(declare-fun a () $i) +(declare-fun b () $i) +(declare-fun c () $i) +(declare-fun d () $i) (assert (and (= a b) (= b c) (or (not (= a c)) (= a d)))) (check-sat)