test cases

5 files changed, 104 insertions, 1 deletions

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 3d68b73cb..881664e83 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -1,4 +1,4 @@
-SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv datatypes lemmas push-pop preprocess
+SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes lemmas push-pop preprocess
 
 BINARY = cvc4
 if PROOF_REGRESSIONS
diff --git a/test/regress/regress0/auflia/Makefile b/test/regress/regress0/auflia/Makefile
new file mode 100644
index 000000000..da859f7e3
--- /dev/null
+++ b/test/regress/regress0/auflia/Makefile
@@ -0,0 +1,8 @@
+topdir = ../../../..
+srcdir = test/regress/regress0/auflia
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check
diff --git a/test/regress/regress0/auflia/Makefile.am b/test/regress/regress0/auflia/Makefile.am
new file mode 100644
index 000000000..314566f87
--- /dev/null
+++ b/test/regress/regress0/auflia/Makefile.am
@@ -0,0 +1,32 @@
+BINARY=cvc4
+if PROOF_REGRESSIONS
+TESTS_ENVIRONMENT = LFSC="$(LFSC) $(LFSCARGS)" @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) --proof @top_builddir@/src/main/$(BINARY)
+else
+TESTS_ENVIRONMENT = @srcdir@/../../run_regression $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)
+endif
+
+# These are run for all build profiles.
+# If a test shouldn't be run in e.g. competition mode,
+# put it below in "TESTS +="
+TESTS =	\
+	bug336.smt2
+
+EXTRA_DIST = $(TESTS)
+
+#if CVC4_BUILD_PROFILE_COMPETITION
+#else
+#TESTS += \
+#	error.cvc
+#endif
+#
+# and make sure to distribute it
+#EXTRA_DIST += \
+#	error.cvc
+
+# synonyms for "check"
+.PHONY: regress regress0 test
+regress regress0 test: check
+
+# do nothing in this subdir
+.PHONY: regress1 regress2 regress3
+regress1 regress2 regress3:
diff --git a/test/regress/regress0/auflia/bug330.smt2 b/test/regress/regress0/auflia/bug330.smt2
new file mode 100644
index 000000000..d05a8b2a0
--- /dev/null
+++ b/test/regress/regress0/auflia/bug330.smt2
@@ -0,0 +1,44 @@
+(set-logic QF_AUFLIA)
+(set-info :source |
+Translated from old SVC processor verification benchmarks.  Contact Clark
+Barrett at barrett@cs.nyu.edu for more information.
+
+This benchmark was automatically translated into SMT-LIB format from
+CVC format using CVC Lite
+|)
+(set-info :smt-lib-version 2.0)
+(set-info :category "industrial")
+(set-info :status unsat)
+(set-info :difficulty | 0 |)
+(declare-fun BUBBLE_EX_INIT () Bool)
+(declare-fun OPCODE_EX_INIT () Int)
+(declare-fun BUBBLE_ID_INIT () Bool)
+(declare-fun RF1_OF (Int) Int)
+(declare-fun INST_ID_INIT () Int)
+(declare-fun DEST_EX_INIT () Int)
+(declare-fun RF2_OF (Int) Int)
+(declare-fun OPCODE_OF (Int) Int)
+(declare-fun STALL_INIT () Bool)
+(declare-fun B_INIT () Int)
+(declare-fun plus (Int Int) Int)
+(declare-fun A_INIT () Int)
+(declare-fun SHORT_IMMED_EX_INIT () Int)
+(declare-fun ALU (Int Int Int) Int)
+(declare-fun ALU_OP_OF (Int) Int)
+(declare-fun DEST_MEM_INIT () Int)
+(declare-fun LOAD_FLAG_INIT () Bool)
+(declare-fun DMEM_INIT () (Array Int Int))
+(declare-fun MAR_INIT () Int)
+(declare-fun RESULT_MEM_INIT () Int)
+(declare-fun DEST_WB_INIT () Int)
+(declare-fun REGFILE_INIT () (Array Int Int))
+(declare-fun RESULT_WB_INIT () Int)
+(declare-fun IMEM_INIT () (Array Int Int))
+(declare-fun PC_INIT () Int)
+(declare-fun RF3_OF (Int) Int)
+(declare-fun LONG_IMMED_OF (Int) Int)
+(declare-fun SHORT_IMMED_OF (Int) Int)
+(declare-fun STORE_FLAG_INIT () Bool)
+(assert (let ((?v_53 (ite BUBBLE_EX_INIT false true)) (?v_7 (= OPCODE_EX_INIT 10)) (?v_2 (ite BUBBLE_ID_INIT false true)) (?v_5 (RF1_OF INST_ID_INIT))) (let ((?v_6 (= ?v_5 DEST_EX_INIT)) (?v_11 (RF2_OF INST_ID_INIT))) (let ((?v_46 (= ?v_11 DEST_EX_INIT))) (let ((?v_1 (ite ?v_53 (ite ?v_7 (ite ?v_2 (ite ?v_6 true ?v_46) false) false) false)) (?v_0 (OPCODE_OF INST_ID_INIT))) (let ((?v_3 (= ?v_0 11)) (?v_4 (= ?v_0 12)) (?v_128 (= ?v_5 0)) (?v_69 (= OPCODE_EX_INIT 13))) (let ((?v_8 (ite ?v_7 true ?v_69))) (let ((?v_54 (ite ?v_8 (plus A_INIT SHORT_IMMED_EX_INIT) (ALU (ALU_OP_OF OPCODE_EX_INIT) A_INIT B_INIT)))) (let ((?v_47 (ite ?v_8 B_INIT ?v_54)) (?v_48 (ite LOAD_FLAG_INIT (select DMEM_INIT MAR_INIT) RESULT_MEM_INIT)) (?v_49 (ite (ite (= DEST_WB_INIT 0) false true) (store REGFILE_INIT DEST_WB_INIT RESULT_WB_INIT) REGFILE_INIT))) (let ((?v_51 (ite ?v_128 0 (ite ?v_6 ?v_47 (ite (= ?v_5 DEST_MEM_INIT) ?v_48 (select ?v_49 ?v_5)))))) (let ((?v_37 (ite ?v_2 (ite ?v_3 true (ite ?v_4 (= ?v_51 0) false)) false))) (let ((?v_159 (ite STALL_INIT true (ite ?v_1 true ?v_37))) (?v_113 (ite ?v_3 true ?v_4))) (let ((?v_9 (ite ?v_1 true (ite BUBBLE_ID_INIT true ?v_113)))) (let ((?v_68 (ite ?v_9 false true)) (?v_10 (= ?v_0 10)) (?v_112 (ite ?v_1 BUBBLE_ID_INIT true))) (let ((?v_127 (ite ?v_112 false true)) (?v_43 (= ?v_0 13)) (?v_44 (= ?v_0 14))) (let ((?v_116 (ite (ite ?v_10 true ?v_44) ?v_11 (RF3_OF INST_ID_INIT)))) (let ((?v_13 (ite (ite ?v_9 true ?v_43) 0 ?v_116))) (let ((?v_129 (= ?v_13 ?v_5)) (?v_135 (= ?v_13 ?v_11))) (let ((?v_114 (ite ?v_68 (ite ?v_10 (ite ?v_127 (ite ?v_129 true ?v_135) false) false) false))) (let ((?v_115 (ite ?v_114 true (ite ?v_112 true ?v_113)))) (let ((?v_146 (ite ?v_115 false true)) (?v_118 (ite ?v_114 ?v_112 true))) (let ((?v_132 (ite ?v_118 false true)) (?v_117 (ite (ite ?v_115 true ?v_43) 0 ?v_116))) (let ((?v_133 (= ?v_117 ?v_5)) (?v_142 (= ?v_117 ?v_11))) (let ((?v_119 (ite ?v_146 (ite ?v_10 (ite ?v_132 (ite ?v_133 true ?v_142) false) false) false))) (let ((?v_120 (ite ?v_119 true (ite ?v_118 true ?v_113)))) (let ((?v_156 (ite ?v_120 false true)) (?v_122 (ite ?v_119 ?v_118 true))) (let ((?v_140 (ite ?v_122 false true)) (?v_121 (ite (ite ?v_120 true ?v_43) 0 ?v_116))) (let ((?v_141 (= ?v_121 ?v_5)) (?v_151 (= ?v_121 ?v_11))) (let ((?v_123 (ite ?v_156 (ite ?v_10 (ite ?v_140 (ite ?v_141 true ?v_151) false) false) false))) (let ((?v_124 (ite ?v_123 true (ite ?v_122 true ?v_113))) (?v_149 (ite (ite ?v_123 ?v_122 true) false true))) (let ((?v_125 (ite (ite ?v_124 true ?v_43) 0 ?v_116))) (let ((?v_150 (= ?v_125 ?v_5)) (?v_130 (LONG_IMMED_OF INST_ID_INIT)) (?v_45 (SHORT_IMMED_OF INST_ID_INIT))) (let ((?v_38 (ite ?v_3 (plus ?v_130 PC_INIT) (plus ?v_45 PC_INIT)))) (let ((?v_126 (ite ?v_37 ?v_38 PC_INIT))) (let ((?v_131 (ite ?v_1 PC_INIT ?v_126)) (?v_50 (ite ?v_10 true ?v_43)) (?v_134 (= ?v_11 0))) (let ((?v_52 (ite ?v_44 ?v_45 (ite ?v_134 0 (ite ?v_46 ?v_47 (ite (= ?v_11 DEST_MEM_INIT) ?v_48 (select ?v_49 ?v_11)))))) (?v_137 (ALU_OP_OF ?v_0))) (let ((?v_71 (ite ?v_50 (plus ?v_51 ?v_45) (ALU ?v_137 ?v_51 ?v_52)))) (let ((?v_62 (ite ?v_50 ?v_52 ?v_71)) (?v_70 (ite STORE_FLAG_INIT (store DMEM_INIT MAR_INIT RESULT_MEM_INIT) DMEM_INIT))) (let ((?v_63 (ite (ite ?v_53 ?v_7 false) (select ?v_70 ?v_54) ?v_47)) (?v_64 (ite (ite (= DEST_MEM_INIT 0) false true) (store ?v_49 DEST_MEM_INIT ?v_48) ?v_49))) (let ((?v_136 (ite ?v_128 0 (ite ?v_129 ?v_62 (ite ?v_6 ?v_63 (select ?v_64 ?v_5)))))) (let ((?v_139 (ite ?v_114 ?v_131 (ite (ite ?v_127 (ite ?v_3 true (ite ?v_4 (= ?v_136 0) false)) false) (ite ?v_3 (plus ?v_130 ?v_131) (plus ?v_45 ?v_131)) ?v_131))) (?v_138 (ite ?v_44 ?v_45 (ite ?v_134 0 (ite ?v_135 ?v_62 (ite ?v_46 ?v_63 (select ?v_64 ?v_11))))))) (let ((?v_147 (ite ?v_50 (plus ?v_136 ?v_45) (ALU ?v_137 ?v_136 ?v_138)))) (let ((?v_143 (ite ?v_50 ?v_138 ?v_147)) (?v_85 (ite (ite ?v_53 ?v_69 false) (store ?v_70 ?v_54 ?v_47) ?v_70))) (let ((?v_79 (ite (ite ?v_68 ?v_10 false) (select ?v_85 ?v_71) ?v_62)) (?v_80 (ite (ite (= DEST_EX_INIT 0) false true) (store ?v_64 DEST_EX_INIT ?v_63) ?v_64))) (let ((?v_144 (ite ?v_128 0 (ite ?v_133 ?v_143 (ite ?v_129 ?v_79 (select ?v_80 ?v_5)))))) (let ((?v_148 (ite ?v_119 ?v_139 (ite (ite ?v_132 (ite ?v_3 true (ite ?v_4 (= ?v_144 0) false)) false) (ite ?v_3 (plus ?v_130 ?v_139) (plus ?v_45 ?v_139)) ?v_139))) (?v_145 (ite ?v_44 ?v_45 (ite ?v_134 0 (ite ?v_142 ?v_143 (ite ?v_135 ?v_79 (select ?v_80 ?v_11))))))) (let ((?v_157 (ite ?v_50 (plus ?v_144 ?v_45) (ALU ?v_137 ?v_144 ?v_145)))) (let ((?v_152 (ite ?v_50 ?v_145 ?v_157)) (?v_97 (ite (ite ?v_68 ?v_43 false) (store ?v_85 ?v_71 ?v_62) ?v_85))) (let ((?v_153 (ite (ite ?v_146 ?v_10 false) (select ?v_97 ?v_147) ?v_143)) (?v_93 (ite (ite (= ?v_13 0) false true) (store ?v_80 ?v_13 ?v_79) ?v_80))) (let ((?v_154 (ite ?v_128 0 (ite ?v_141 ?v_152 (ite ?v_133 ?v_153 (select ?v_93 ?v_5)))))) (let ((?v_158 (ite ?v_123 ?v_148 (ite (ite ?v_140 (ite ?v_3 true (ite ?v_4 (= ?v_154 0) false)) false) (ite ?v_3 (plus ?v_130 ?v_148) (plus ?v_45 ?v_148)) ?v_148))) (?v_155 (ite ?v_44 ?v_45 (ite ?v_134 0 (ite ?v_151 ?v_152 (ite ?v_142 ?v_153 (select ?v_93 ?v_11)))))) (?v_165 (ite (ite (= ?v_117 0) false true) (store ?v_93 ?v_117 ?v_153) ?v_93))) (let ((?v_160 (ite (ite (ite ?v_124 false true) (ite ?v_10 (ite ?v_149 (ite ?v_150 true (= ?v_125 ?v_11)) false) false) false) ?v_158 (ite (ite ?v_149 (ite ?v_3 true (ite ?v_4 (= (ite ?v_128 0 (ite ?v_150 (ite ?v_50 ?v_155 (ite ?v_50 (plus ?v_154 ?v_45) (ALU ?v_137 ?v_154 ?v_155))) (ite ?v_141 (ite (ite ?v_156 ?v_10 false) (select (ite (ite ?v_146 ?v_43 false) (store ?v_97 ?v_147 ?v_143) ?v_97) ?v_157) ?v_152) (select ?v_165 ?v_5)))) 0) false)) false) (ite ?v_3 (plus ?v_130 ?v_158) (plus ?v_45 ?v_158)) ?v_158)))) (let ((?v_163 (select IMEM_INIT ?v_160))) (let ((?v_161 (OPCODE_OF ?v_163)) (?v_164 (plus 4 ?v_160))) (let ((?v_162 (ite ?v_159 ?v_160 ?v_164)) (?v_166 (RF1_OF ?v_163)) (?v_14 (ite ?v_1 BUBBLE_ID_INIT (ite STALL_INIT true ?v_37)))) (let ((?v_39 (ite ?v_14 false true)) (?v_12 (ite ?v_1 INST_ID_INIT (ite STALL_INIT INST_ID_INIT (select IMEM_INIT PC_INIT))))) (let ((?v_20 (RF1_OF ?v_12))) (let ((?v_42 (= ?v_20 ?v_13)) (?v_19 (RF2_OF ?v_12))) (let ((?v_61 (= ?v_19 ?v_13))) (let ((?v_16 (ite ?v_68 (ite ?v_10 (ite ?v_39 (ite ?v_42 true ?v_61) false) false) false)) (?v_15 (OPCODE_OF ?v_12))) (let ((?v_40 (= ?v_15 11)) (?v_41 (= ?v_15 12))) (let ((?v_23 (ite ?v_40 true ?v_41))) (let ((?v_17 (ite ?v_16 true (ite ?v_14 true ?v_23)))) (let ((?v_84 (ite ?v_17 false true)) (?v_18 (= ?v_15 10)) (?v_22 (ite ?v_16 ?v_14 true))) (let ((?v_56 (ite ?v_22 false true)) (?v_26 (= ?v_15 13)) (?v_59 (= ?v_15 14))) (let ((?v_27 (ite (ite ?v_18 true ?v_59) ?v_19 (RF3_OF ?v_12)))) (let ((?v_21 (ite (ite ?v_17 true ?v_26) 0 ?v_27))) (let ((?v_58 (= ?v_21 ?v_20)) (?v_77 (= ?v_21 ?v_19))) (let ((?v_24 (ite ?v_84 (ite ?v_18 (ite ?v_56 (ite ?v_58 true ?v_77) false) false) false))) (let ((?v_25 (ite ?v_24 true (ite ?v_22 true ?v_23)))) (let ((?v_96 (ite ?v_25 false true)) (?v_29 (ite ?v_24 ?v_22 true))) (let ((?v_74 (ite ?v_29 false true)) (?v_28 (ite (ite ?v_25 true ?v_26) 0 ?v_27))) (let ((?v_75 (= ?v_28 ?v_20)) (?v_90 (= ?v_28 ?v_19))) (let ((?v_30 (ite ?v_96 (ite ?v_18 (ite ?v_74 (ite ?v_75 true ?v_90) false) false) false))) (let ((?v_31 (ite ?v_30 true (ite ?v_29 true ?v_23)))) (let ((?v_108 (ite ?v_31 false true)) (?v_33 (ite ?v_30 ?v_29 true))) (let ((?v_88 (ite ?v_33 false true)) (?v_32 (ite (ite ?v_31 true ?v_26) 0 ?v_27))) (let ((?v_89 (= ?v_32 ?v_20)) (?v_102 (= ?v_32 ?v_19))) (let ((?v_34 (ite ?v_108 (ite ?v_18 (ite ?v_88 (ite ?v_89 true ?v_102) false) false) false))) (let ((?v_35 (ite ?v_34 true (ite ?v_33 true ?v_23))) (?v_100 (ite (ite ?v_34 ?v_33 true) false true))) (let ((?v_36 (ite (ite ?v_35 true ?v_26) 0 ?v_27))) (let ((?v_101 (= ?v_36 ?v_20)) (?v_55 (ite ?v_1 PC_INIT (ite STALL_INIT ?v_126 (ite ?v_37 ?v_38 (plus 4 PC_INIT))))) (?v_57 (= ?v_20 0))) (let ((?v_66 (ite ?v_57 0 (ite ?v_42 ?v_62 (ite (= ?v_20 DEST_EX_INIT) ?v_63 (select ?v_64 ?v_20))))) (?v_72 (LONG_IMMED_OF ?v_12)) (?v_60 (SHORT_IMMED_OF ?v_12))) (let ((?v_73 (ite ?v_16 ?v_55 (ite (ite ?v_39 (ite ?v_40 true (ite ?v_41 (= ?v_66 0) false)) false) (ite ?v_40 (plus ?v_72 ?v_55) (plus ?v_60 ?v_55)) ?v_55))) (?v_65 (ite ?v_18 true ?v_26)) (?v_76 (= ?v_19 0))) (let ((?v_67 (ite ?v_59 ?v_60 (ite ?v_76 0 (ite ?v_61 ?v_62 (ite (= ?v_19 DEST_EX_INIT) ?v_63 (select ?v_64 ?v_19)))))) (?v_82 (ALU_OP_OF ?v_15))) (let ((?v_86 (ite ?v_65 (plus ?v_66 ?v_60) (ALU ?v_82 ?v_66 ?v_67)))) (let ((?v_78 (ite ?v_65 ?v_67 ?v_86))) (let ((?v_81 (ite ?v_57 0 (ite ?v_58 ?v_78 (ite ?v_42 ?v_79 (select ?v_80 ?v_20)))))) (let ((?v_87 (ite ?v_24 ?v_73 (ite (ite ?v_56 (ite ?v_40 true (ite ?v_41 (= ?v_81 0) false)) false) (ite ?v_40 (plus ?v_72 ?v_73) (plus ?v_60 ?v_73)) ?v_73))) (?v_83 (ite ?v_59 ?v_60 (ite ?v_76 0 (ite ?v_77 ?v_78 (ite ?v_61 ?v_79 (select ?v_80 ?v_19))))))) (let ((?v_98 (ite ?v_65 (plus ?v_81 ?v_60) (ALU ?v_82 ?v_81 ?v_83)))) (let ((?v_91 (ite ?v_65 ?v_83 ?v_98)) (?v_92 (ite (ite ?v_84 ?v_18 false) (select ?v_97 ?v_86) ?v_78))) (let ((?v_94 (ite ?v_57 0 (ite ?v_75 ?v_91 (ite ?v_58 ?v_92 (select ?v_93 ?v_20)))))) (let ((?v_99 (ite ?v_30 ?v_87 (ite (ite ?v_74 (ite ?v_40 true (ite ?v_41 (= ?v_94 0) false)) false) (ite ?v_40 (plus ?v_72 ?v_87) (plus ?v_60 ?v_87)) ?v_87))) (?v_95 (ite ?v_59 ?v_60 (ite ?v_76 0 (ite ?v_90 ?v_91 (ite ?v_77 ?v_92 (select ?v_93 ?v_19))))))) (let ((?v_110 (ite ?v_65 (plus ?v_94 ?v_60) (ALU ?v_82 ?v_94 ?v_95)))) (let ((?v_103 (ite ?v_65 ?v_95 ?v_110)) (?v_109 (ite (ite ?v_84 ?v_26 false) (store ?v_97 ?v_86 ?v_78) ?v_97))) (let ((?v_104 (ite (ite ?v_96 ?v_18 false) (select ?v_109 ?v_98) ?v_91)) (?v_105 (ite (ite (= ?v_21 0) false true) (store ?v_93 ?v_21 ?v_92) ?v_93))) (let ((?v_106 (ite ?v_57 0 (ite ?v_89 ?v_103 (ite ?v_75 ?v_104 (select ?v_105 ?v_20)))))) (let ((?v_111 (ite ?v_34 ?v_99 (ite (ite ?v_88 (ite ?v_40 true (ite ?v_41 (= ?v_106 0) false)) false) (ite ?v_40 (plus ?v_72 ?v_99) (plus ?v_60 ?v_99)) ?v_99))) (?v_107 (ite ?v_59 ?v_60 (ite ?v_76 0 (ite ?v_102 ?v_103 (ite ?v_90 ?v_104 (select ?v_105 ?v_19))))))) (not (= (ite (ite (ite ?v_35 false true) (ite ?v_18 (ite ?v_100 (ite ?v_101 true (= ?v_36 ?v_19)) false) false) false) ?v_111 (ite (ite ?v_100 (ite ?v_40 true (ite ?v_41 (= (ite ?v_57 0 (ite ?v_101 (ite ?v_65 ?v_107 (ite ?v_65 (plus ?v_106 ?v_60) (ALU ?v_82 ?v_106 ?v_107))) (ite ?v_89 (ite (ite ?v_108 ?v_18 false) (select (ite (ite ?v_96 ?v_26 false) (store ?v_109 ?v_98 ?v_91) ?v_109) ?v_110) ?v_103) (select (ite (ite (= ?v_28 0) false true) (store ?v_105 ?v_28 ?v_104) ?v_105) ?v_20)))) 0) false)) false) (ite ?v_40 (plus ?v_72 ?v_111) (plus ?v_60 ?v_111)) ?v_111)) (ite (ite ?v_159 false true) (ite (= ?v_161 10) ?v_162 (ite (= ?v_161 13) ?v_162 (ite (= ?v_161 11) (plus (LONG_IMMED_OF ?v_163) ?v_164) (ite (= ?v_161 12) (ite (= (ite (= ?v_166 0) 0 (select ?v_165 ?v_166)) 0) (plus (SHORT_IMMED_OF ?v_163) ?v_164) ?v_164) ?v_162)))) ?v_162)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/auflia/bug336.smt2 b/test/regress/regress0/auflia/bug336.smt2
new file mode 100644
index 000000000..f8909c23c
--- /dev/null
+++ b/test/regress/regress0/auflia/bug336.smt2
@@ -0,0 +1,19 @@
+(set-logic QF_AUFLIA)
+(set-info :source | This is based on an example in Section 6.2 of "A Decision
+Procedure for an Extensional Theory of Arrays" by Stump, Barrett, Dill, and
+Levitt. |)
+(set-info :smt-lib-version 2.0)
+(set-info :category "check")
+(set-info :status unsat)
+(set-info :notes |This benchmark is designed to require an array DP to propagate a properly entailed disjunction of equalities between shared terms.|)
+(declare-fun a () (Array Int Int))
+(declare-fun b () (Array Int Int))
+(declare-fun v () Int)
+(declare-fun w () Int)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(declare-fun g ((Array Int Int)) Int)
+(declare-fun f (Int) Int)
+(assert (and (= (store a x v) b) (= (store a y w) b) (not (= (f x) (f y))) (not (= (g a) (g b)))))
+(check-sat)
+(exit)