1 files changed, 82 insertions, 0 deletions
diff --git a/src/lfsc/tests/swap3.smt2 b/src/lfsc/tests/swap3.smt2
new file mode 100644
index 0000000..cade13f
--- /dev/null
+++ b/src/lfsc/tests/swap3.smt2
@@ -0,0 +1,82 @@
+(set-logic QF_AUFLIA)
+(set-info :source |
+Benchmarks used in the followin paper:
+Big proof engines as little proof engines: new results on rewrite-based satisfiability procedure
+Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Stephan Schulz. 
+PDPAR'05
+http://www.ai.dist.unige.it/pdpar05/
+
+
+|)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun a_705 () (Array Int Int))
+(declare-fun a_707 () (Array Int Int))
+(declare-fun a_709 () (Array Int Int))
+(declare-fun a_711 () (Array Int Int))
+(declare-fun a_713 () (Array Int Int))
+(declare-fun a_715 () (Array Int Int))
+(declare-fun a_717 () (Array Int Int))
+(declare-fun a_719 () (Array Int Int))
+(declare-fun a_721 () (Array Int Int))
+(declare-fun a_723 () (Array Int Int))
+(declare-fun a_725 () (Array Int Int))
+(declare-fun a_727 () (Array Int Int))
+(declare-fun a_728 () (Array Int Int))
+(declare-fun a_729 () (Array Int Int))
+(declare-fun e_704 () Int)
+(declare-fun e_706 () Int)
+(declare-fun e_708 () Int)
+(declare-fun e_710 () Int)
+(declare-fun e_712 () Int)
+(declare-fun e_714 () Int)
+(declare-fun e_716 () Int)
+(declare-fun e_718 () Int)
+(declare-fun e_720 () Int)
+(declare-fun e_722 () Int)
+(declare-fun e_724 () Int)
+(declare-fun e_726 () Int)
+(declare-fun e_731 () Int)
+(declare-fun e_732 () Int)
+(declare-fun i_730 () Int)
+(declare-fun a1 () (Array Int Int))
+(declare-fun i0 () Int)
+(declare-fun i1 () Int)
+(declare-fun i2 () Int)
+(declare-fun i3 () Int)
+(declare-fun i4 () Int)
+(declare-fun i5 () Int)
+(declare-fun sk ((Array Int Int) (Array Int Int)) Int)
+(assert (= a_705 (store a1 i4 e_704)))
+(assert (= a_707 (store a_705 i2 e_706)))
+(assert (= a_709 (store a_707 i1 e_708)))
+(assert (= a_711 (store a_709 i4 e_710)))
+(assert (= a_713 (store a_711 i5 e_712)))
+(assert (= a_715 (store a_713 i3 e_714)))
+(assert (= a_717 (store a_715 i4 e_716)))
+(assert (= a_719 (store a_717 i2 e_718)))
+(assert (= a_721 (store a_719 i1 e_720)))
+(assert (= a_723 (store a_721 i0 e_722)))
+(assert (= a_725 (store a_723 i5 e_724)))
+(assert (= a_727 (store a_725 i2 e_726)))
+(assert (= a_728 (store a_723 i2 e_726)))
+(assert (= a_729 (store a_728 i5 e_724)))
+(assert (= e_704 (select a1 i2)))
+(assert (= e_706 (select a1 i4)))
+(assert (= e_708 (select a_707 i4)))
+(assert (= e_710 (select a_707 i1)))
+(assert (= e_712 (select a_711 i3)))
+(assert (= e_714 (select a_711 i5)))
+(assert (= e_716 (select a_715 i2)))
+(assert (= e_718 (select a_715 i4)))
+(assert (= e_720 (select a_719 i0)))
+(assert (= e_722 (select a_719 i1)))
+(assert (= e_724 (select a_723 i2)))
+(assert (= e_726 (select a_723 i5)))
+(assert (= e_731 (select a_727 i_730)))
+(assert (= e_732 (select a_729 i_730)))
+(assert (= i_730 (sk a_727 a_729)))
+(assert (not (= e_731 e_732)))
+(check-sat)
+(exit)