From c5f23e32b978ea46f30c141e8f030f9e795864ac Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Mon, 11 Jun 2018 21:56:34 -0500 Subject: [PATCH] test: proper smtlib for QFUF problems --- tests/sat/test-007.smt2 | 4 ++++ tests/sat/test-010.smt2 | 5 +++++ 2 files changed, 9 insertions(+) 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)