@@ -719,6 +719,23 @@ tests/regress/mantis/0032.smt2
719719tests/regress/mantis/0035.smt2
720720tests/regress/mantis/0036.smt2
721721tests/regress/mantis/0037.smt2 [ --incremental ]
722+ tests/regress/mcsat/arrays/arr1.smt2 [ --mcsat ]
723+ tests/regress/mcsat/arrays/arrays_extensionality_no_selects_unsat.smt2 [ --mcsat --incremental ]
724+ tests/regress/mcsat/arrays/arrays_extensionality_no_selects.smt2 [ --mcsat --incremental ]
725+ tests/regress/mcsat/arrays/arrays0.smt2 [ --mcsat ]
726+ tests/regress/mcsat/arrays/arrays1.smt2 [ --mcsat ]
727+ tests/regress/mcsat/arrays/arrays2.smt2 [ --mcsat ]
728+ tests/regress/mcsat/arrays/arrays3.smt2 [ --mcsat ]
729+ tests/regress/mcsat/arrays/arrays4.smt2 [ --mcsat ]
730+ tests/regress/mcsat/arrays/aviad_true-alloca_true-termination.c.i.partial.smt2 [ --mcsat --incremental ]
731+ tests/regress/mcsat/arrays/bool-array.smt2 [ --mcsat ]
732+ tests/regress/mcsat/arrays/example_weqa.smt2 [ --mcsat ]
733+ tests/regress/mcsat/arrays/linux-4.0-rc1---kernel--locking--locktorture.ko.cil_smt-query.1.smt2 [ --mcsat --incremental ]
734+ tests/regress/mcsat/arrays/read_over_weak_eq_lemma_2.smt2 [ --mcsat --incremental ]
735+ tests/regress/mcsat/arrays/read_over_weak_eq_lemma.smt2 [ --mcsat --incremental ]
736+ tests/regress/mcsat/arrays/storecomm_t2_np_sf_ai_00060_009.cvc.smt2 [ --mcsat --incremental ]
737+ tests/regress/mcsat/arrays/trivially_unsat.smt2 [ --mcsat --incremental ]
738+ tests/regress/mcsat/arrays/unsat_with_decisions.smt2 [ --mcsat --incremental ]
722739tests/regress/mcsat/bool/bool_00.smt2 [ --mcsat ]
723740tests/regress/mcsat/bool/bool_01.smt2 [ --mcsat ]
724741tests/regress/mcsat/bool/bool_02.smt2 [ --mcsat ]
@@ -761,12 +778,43 @@ tests/regress/mcsat/bool/bool_random_200vars.07.smt2 [ --mcsat ]
761778tests/regress/mcsat/bool/bool_random_200vars.08.smt2 [ --mcsat ]
762779tests/regress/mcsat/bool/bool_random_200vars.09.smt2 [ --mcsat ]
763780tests/regress/mcsat/bool/bool_random_200vars.10.smt2 [ --mcsat ]
764- tests/regress/mcsat/ite/ite_00.smt2
765- tests/regress/mcsat/ite/ite_01.smt2
766- tests/regress/mcsat/ite/ite_02.smt2
767- tests/regress/mcsat/ite/ite_03.smt2
781+ tests/regress/mcsat/bv/bin_libmsrpc_vc1225397.smt2 [ --mcsat ]
782+ tests/regress/mcsat/bv/simple_processors_002_002_0008.smt2 [ --mcsat --mcsat-bv-var-size=8 ]
783+ tests/regress/mcsat/bv/test_bvarray_bool2.smt2 [ --mcsat ]
784+ tests/regress/mcsat/bv/try5_small_true_functions_flanagansaxe_mv.dev_info_compare.il.flanagansaxe.smt2 [ --mcsat ]
785+ tests/regress/mcsat/bv/unconstrained05.smt2 [ --mcsat ]
786+ tests/regress/mcsat/bv/uum4.smt2 [ --mcsat ]
787+ tests/regress/mcsat/bv/xinetd_xinetd_vc18132.smt2 [ --mcsat ]
788+ tests/regress/mcsat/bv/y.smt2 [ --mcsat ]
789+ tests/regress/mcsat/ff/compilation-deterministic-last-02v-000t-ff-zokref-255b-ands.smt2
790+ tests/regress/mcsat/ff/compilation-deterministic-last-02v-004t-ff-circ-12b-0s.smt2
791+ tests/regress/mcsat/ff/compilation-sound-last-02v-004t-ff-circ-5b-0s.smt2
792+ tests/regress/mcsat/ff/compilation-sound-none-02v-004t-ff-circ-5b-0s.smt2
793+ tests/regress/mcsat/ff/invalid-fieldsize.smt2
794+ tests/regress/mcsat/ff/testdata_i_13_8_8.001.smt2
795+ tests/regress/mcsat/ff/testdata_i_3_8_8.004.smt2
796+ tests/regress/mcsat/ff/testdata_i_3_8_8.008.smt2
797+ tests/regress/mcsat/ff/testdata_i_3_8_8.016.smt2
798+ tests/regress/mcsat/ff/testdata_r_13_32_8.012.smt2
799+ tests/regress/mcsat/ff/testdata_r_211_16_8.016.smt2
800+ tests/regress/mcsat/ff/testdata_r_211_16_8.021.smt2
801+ tests/regress/mcsat/ite/ite_00.smt2 [ --mcsat ]
802+ tests/regress/mcsat/ite/ite_01.smt2 [ --mcsat ]
803+ tests/regress/mcsat/ite/ite_02.smt2 [ --mcsat ]
804+ tests/regress/mcsat/ite/ite_03.smt2 [ --mcsat ]
805+ tests/regress/mcsat/lia/lira_00.smt2 [ --mcsat ]
806+ tests/regress/mcsat/lra/fuzz01.smt2 [ --mcsat --incremental ]
807+ tests/regress/mcsat/lra/fuzz02.smt2 [ --mcsat --incremental ]
808+ tests/regress/mcsat/lra/fuzz04.smt2 [ --mcsat --incremental ]
809+ tests/regress/mcsat/lra/fuzz05.smt2 [ --mcsat --incremental ]
810+ tests/regress/mcsat/lra/fuzz06.smt2 [ --mcsat --incremental ]
811+ tests/regress/mcsat/lra/fuzz07.smt2 [ --mcsat --incremental ]
812+ tests/regress/mcsat/lra/fuzz08.smt2 [ --mcsat--incremental ]
813+ tests/regress/mcsat/lra/fuzz09.smt2 [ --mcsat --incremental ]
768814tests/regress/mcsat/lra/incremental/fail.00.smt2 [ --incremental --mcsat ]
769815tests/regress/mcsat/lra/incremental/MOESI_all_e3_2032_e3_2788.ec.2.smt2 [ --incremental --mcsat ]
816+ tests/regress/mcsat/lra/issue188.smt2 [ --mcsat --incremental ]
817+ tests/regress/mcsat/lra/issue270.smt2 [ --mcsat --incremental ]
770818tests/regress/mcsat/nia/div_00.smt2
771819tests/regress/mcsat/nia/div_01.smt2
772820tests/regress/mcsat/nia/div_02.smt2
@@ -879,12 +927,12 @@ tests/regress/mcsat/uf/incremental/ufnra_01.smt2 [ --incremental --mcsat ]
879927tests/regress/mcsat/uf/incremental/ufnra_04.smt2 [ --incremental --mcsat ]
880928tests/regress/mcsat/uf/incremental/ufnra_05.smt2 [ --incremental --mcsat ]
881929tests/regress/mcsat/uf/incremental/ufnra_06.smt2 [ --incremental --mcsat ]
882- tests/regress/mcsat/uf/PEQ012_size3.smt2
883- tests/regress/mcsat/uf/uf_00.smt2
884- tests/regress/mcsat/uf/uf_01.smt2
885- tests/regress/mcsat/uf/uf_02.smt2
886- tests/regress/mcsat/uf/uf_03.smt2
887- tests/regress/mcsat/uf/uf_04.smt2
930+ tests/regress/mcsat/uf/PEQ012_size3.smt2 [ --mcsat ]
931+ tests/regress/mcsat/uf/uf_00.smt2 [ --mcsat ]
932+ tests/regress/mcsat/uf/uf_01.smt2 [ --mcsat ]
933+ tests/regress/mcsat/uf/uf_02.smt2 [ --mcsat ]
934+ tests/regress/mcsat/uf/uf_03.smt2 [ --mcsat ]
935+ tests/regress/mcsat/uf/uf_04.smt2 [ --mcsat ]
888936tests/regress/mcsat/uf/uf_05.smt2 [ --mcsat ]
889937tests/regress/mcsat/uf/ufnra_00.smt2
890938tests/regress/mcsat/uf/ufnra_01.smt2
@@ -893,9 +941,14 @@ tests/regress/mcsat/uf/ufnra_03.smt2
893941tests/regress/mcsat/uf/ufnra_04.smt2
894942tests/regress/mcsat/uf/ufnra_05.smt2
895943tests/regress/mcsat/uf/ufnra_06.smt2
896- tests/regress/mcsat/uf/z3.630166.smt2
897- tests/regress/mcsat/uf/z3.631468.smt2
898- tests/regress/mcsat/uf/z3.641736.smt2
944+ tests/regress/mcsat/uf/z3.630166.smt2 [ --mcsat ]
945+ tests/regress/mcsat/uf/z3.631468.smt2 [ --mcsat ]
946+ tests/regress/mcsat/uf/z3.641736.smt2 [ --mcsat ]
947+ tests/regress/mcsat/wd/issue311a.smt2 [ --mcsat ]
948+ tests/regress/mcsat/wd/issue311b.smt2 [ --mcsat ]
949+ tests/regress/mcsat/wd/issue311c.smt2 [ --mcsat ]
950+ tests/regress/mcsat/wd/issue311d.smt2 [ --mcsat ]
951+ tests/regress/mcsat/wd/issue311h.smt2 [ --mcsat ]
899952tests/regress/tptp/tptp_830326_ARI376=1.smt2
900953tests/regress/tptp/tptp_830327_ARI369=1.smt2
901954tests/regress/tptp/tptp_830328_ARI355=1.smt2
@@ -922,8 +975,8 @@ tests/regress/tptp/tptp_830348_ARI375=1.smt2
922975tests/regress/tptp/tptp_830349_ARI384=1.smt2
923976tests/regress/tptp/tptp_830350_ARI382=1.smt2
924977tests/regress/wd/c6b_i.smt2
925- tests/regress/wd/c6b_succ_i.smt2
926978tests/regress/wd/c6b_succ_i_unint.smt2
979+ tests/regress/wd/c6b_succ_i.smt2
927980tests/regress/wd/cliffordwolf2.smt2 [ --incremental ]
928981tests/regress/wd/parser-bug-reduced.smt2
929982tests/regress/wd/prp-1-22.smt2
0 commit comments