Arrays: Add regression tests

usi-verification-and-security · Jul 22, 2022 · b1c4a0f · b1c4a0f
1 parent ab7ddf0
commit b1c4a0f
Show file tree

Hide file tree

Showing 6 changed files with 23 additions and 0 deletions.
diff --git a/regression/QF_AX/arrays_extensionality_no_selects.smt2 b/regression/QF_AX/arrays_extensionality_no_selects.smt2
@@ -0,0 +1,9 @@
+(set-logic QF_AX)
+(set-info :status sat)
+(set-info :smt-lib-version 2.6)
+(declare-sort I 0)
+(declare-sort E 0)
+(declare-fun S () (Array I E))
+(declare-fun SS () (Array I E))
+(assert (= S SS))
+(check-sat)
diff --git a/regression/QF_AX/arrays_extensionality_no_selects.smt2.expected.err b/regression/QF_AX/arrays_extensionality_no_selects.smt2.expected.err
diff --git a/regression/QF_AX/arrays_extensionality_no_selects.smt2.expected.out b/regression/QF_AX/arrays_extensionality_no_selects.smt2.expected.out
@@ -0,0 +1 @@
+sat
diff --git a/regression/QF_AX/arrays_extensionality_no_selects_unsat.smt2 b/regression/QF_AX/arrays_extensionality_no_selects_unsat.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_AX)
+(set-info :status unsat)
+(set-info :smt-lib-version 2.6)
+(declare-sort I 0)
+(declare-sort E 0)
+(declare-fun S () (Array I E))
+(declare-fun SS () (Array I E))
+(declare-fun SSS () (Array I E))
+(assert (= S SS))
+(assert (= SS SSS))
+(assert (not (= S SSS)))
+(check-sat)
diff --git a/regression/QF_AX/arrays_extensionality_no_selects_unsat.smt2.expected.err b/regression/QF_AX/arrays_extensionality_no_selects_unsat.smt2.expected.err
diff --git a/regression/QF_AX/arrays_extensionality_no_selects_unsat.smt2.expected.out b/regression/QF_AX/arrays_extensionality_no_selects_unsat.smt2.expected.out
@@ -0,0 +1 @@
+unsat