python = import('python').find_installation() run_regress_script = find_program('run-test-case.py') tests_smt2 = [ ['backtrack/assertion_stack1.smt2'], ['backtrack/assertion_stack2.smt2'], ['backtrack/assertion_stack3.smt2'], ['backtrack/assertion_stack4.smt2'], ['check/regr_cm1.smt2'], ['check/regr_cm10.smt2'], ['check/regr_cm11.smt2'], ['check/regr_cm12.smt2'], ['check/regr_cm13.smt2'], ['check/regr_cm14.smt2'], ['check/regr_cm2.smt2'], ['check/regr_cm3.smt2'], ['check/regr_cm4.smt2'], ['check/regr_cm5.smt2'], ['check/regr_cm6.smt2'], ['check/regr_cm7.smt2'], ['check/regr_cm8.smt2'], ['check/regr_cm9.smt2'], ['check/regr_uc1.smt2'], ['get-model/regr-5smod3.btor.smt2'], ['get-model/regr-5srem3.btor.smt2'], ['get-model/regr-6smod3.btor.smt2'], ['get-model/regr-6srem3.btor.smt2'], ['get-model/regr5smod-3.btor.smt2'], ['get-model/regr5srem-3.btor.smt2'], ['get-model/regr6smod-3.btor.smt2'], ['get-model/regr6srem-3.btor.smt2'], ['get-model/smtandvar.smt2'], ['get-model/smtiff.smt2'], ['get-model/smtnotvar.smt2'], ['get-model/smtor.smt2'], ['get-model/smtvar.smt2'], ['get-model/smtxor.smt2'], ['get-unsat-assumptions/array-smtextarrayaxiom3.smt2'], ['get-unsat-assumptions/bv-count03plus2inc.smt2'], ['get-unsat-assumptions/fp_misc.smt2'], ['get-unsat-assumptions/fp_misc2.smt2'], ['get-unsat-assumptions/fp_misc3.smt2'], ['get-unsat-core/array-smtextarrayaxiom3.smt2'], ['get-unsat-core/bv-count03plus2inc.smt2'], ['get-unsat-core/fp_misc.smt2'], ['get-value/array-issue32.smt2'], ['get-value/array-issue35.smt2'], ['get-value/array.smt2'], ['get-value/bv1.smt2'], ['get-value/bv2.smt2'], ['get-value/bv3.smt2'], ['get-value/bv3.smt2'], ['get-value/fp_rational.smt2'], ['get-value/fp_real.smt2'], ['get-value/fp_regr9.smt2'], ['parser/echo.smt2'], ['parser/issue59-1.smt2'], ['parser/issue59-2.smt2'], ['parser/issue66.smt2'], ['parser/let.smt2'], ['parser/regmismatch.smt2'], ['parser/reset.smt2'], ['parser/reset_assertions.smt2'], ['parser/unsupported_opt_attr.smt2'], ['parser/smt2perr000.smt2'], ['parser/smt2perr001.smt2'], ['parser/smt2perr002.smt2'], ['parser/smt2perr003.smt2'], ['parser/smt2perr004.smt2'], ['parser/smt2perr005.smt2'], ['parser/smt2perr006.smt2'], ['parser/smt2perr007.smt2'], ['parser/smt2perr008.smt2'], ['parser/smt2perr009.smt2'], ['parser/smt2perr010.smt2'], ['parser/smt2perr011.smt2'], ['parser/smt2perr012.smt2'], ['parser/smt2perr013.smt2'], ['parser/smt2perr014.smt2'], ['parser/smt2perr015.smt2'], ['parser/smt2perr016.smt2'], ['parser/smt2perr017.smt2'], ['parser/smt2perr018.smt2'], ['parser/smt2perr019.smt2'], ['parser/smt2perr020.smt2'], ['parser/smt2perr021.smt2'], ['parser/smt2perr022.smt2'], ['parser/smt2perr023.smt2'], ['parser/smt2perr024.smt2'], ['parser/smt2perr025.smt2'], ['parser/smt2perr026.smt2'], ['parser/smt2perr027.smt2'], ['parser/smt2perr028.smt2'], ['parser/smt2perr029.smt2'], ['parser/smt2perr030.smt2'], ['parser/smt2perr031.smt2'], ['parser/smt2perr032.smt2'], ['parser/smt2perr033.smt2'], ['parser/smt2perr034.smt2'], ['parser/smt2perr035.smt2'], ['parser/smt2perr036.smt2'], ['parser/smt2perr037.smt2'], ['parser/smt2perr038.smt2'], ['parser/smt2perr039.smt2'], ['parser/smt2perr040.smt2'], ['parser/smt2perr041.smt2'], ['parser/smt2perr042.smt2'], ['parser/smt2perr043.smt2'], ['parser/smt2perr044.smt2'], ['parser/smt2perr045.smt2'], ['parser/smt2perr046.smt2'], ['parser/smt2perr047.smt2'], ['parser/smt2perr048.smt2'], ['parser/smt2perr049.smt2'], ['parser/smt2perr050.smt2'], ['parser/smt2perr051.smt2'], ['parser/smt2perr052.smt2'], ['parser/smt2perr053.smt2'], ['parser/smt2perr054.smt2'], ['parser/smt2perr055.smt2'], ['parser/smt2perr056.smt2'], ['parser/smt2perr057.smt2'], ['parser/smt2perr058.smt2'], ['parser/smt2perr059.smt2'], ['parser/smt2perr060.smt2'], ['parser/smt2perr061.smt2'], ['parser/smt2perr062.smt2'], ['parser/smt2perr063.smt2'], ['parser/smt2perr064.smt2'], ['parser/smt2perr065.smt2'], ['parser/smt2perr066.smt2'], ['parser/smt2perr067.smt2'], ['parser/smt2perr068.smt2'], ['parser/smt2perr069.smt2'], ['parser/smt2perr070.smt2'], ['parser/smt2perr071.smt2'], ['parser/smt2perr072.smt2'], ['parser/smt2perr073.smt2'], ['parser/smt2perr074.smt2'], ['parser/smt2perr075.smt2'], ['parser/smt2perr076.smt2'], ['parser/smt2perr077.smt2'], ['parser/smt2perr078.smt2'], ['parser/smt2perr079.smt2'], ['parser/smt2perr080.smt2'], ['parser/smt2perr081.smt2'], ['parser/smt2perr082.smt2'], ['parser/smt2perr083.smt2'], ['parser/smt2perr084.smt2'], ['parser/smt2perr085.smt2'], ['parser/smt2perr086.smt2'], ['parser/smt2perr087.smt2'], ['parser/smt2perr088.smt2'], ['parser/smt2perr089.smt2'], ['parser/smt2perr090.smt2'], ['parser/smt2perr091.smt2'], ['parser/smt2perr092.smt2'], ['parser/smt2perr093.smt2'], ['parser/smt2perr094.smt2'], ['parser/smt2perr095.smt2'], ['parser/smt2perr096.smt2'], ['parser/smt2perr097.smt2'], ['parser/smt2perr098.smt2'], ['parser/smt2perr099.smt2'], ['parser/smt2perr100.smt2'], ['parser/smt2perr101.smt2'], ['parser/smt2perr102.smt2'], ['parser/smt2perr103.smt2'], ['parser/smt2perr104.smt2'], ['parser/smt2perr105.smt2'], ['parser/smt2perr106.smt2'], ['parser/smt2perr107.smt2'], ['parser/smt2perr108.smt2'], ['parser/smt2perr109.smt2'], ['parser/smt2perr110.smt2'], ['parser/smt2perr111.smt2'], ['parser/smt2perr112.smt2'], ['parser/smt2perr113.smt2'], ['parser/smt2perr114.smt2'], ['parser/smt2perr115.smt2'], ['parser/smt2perr116.smt2'], ['parser/smt2perr117.smt2'], ['parser/smt2perr118.smt2'], ['parser/smt2perr119.smt2'], ['parser/smt2perr120.smt2'], ['parser/smt2perr121.smt2'], ['parser/smt2perr122.smt2'], ['parser/smt2perr123.smt2'], ['parser/smt2perr124.smt2'], ['parser/smt2perr125.smt2'], ['parser/smt2perr126.smt2'], ['parser/smt2perr127.smt2'], ['parser/smt2perr128.smt2'], ['parser/smt2perr129.smt2'], ['parser/smt2perr130.smt2'], ['parser/smt2perr131.smt2'], ['parser/smt2perr132.smt2'], ['parser/smt2perr133.smt2'], ['parser/smt2perr134.smt2'], ['parser/smt2perr135.smt2'], ['parser/smt2perr136.smt2'], ['parser/smt2perr137.smt2'], ['parser/smt2perr138.smt2'], ['parser/smt2perr139.smt2'], ['parser/smt2perr140.smt2'], ['parser/smt2perr141.smt2'], ['parser/smt2perr142.smt2'], ['parser/smt2perr143.smt2'], ['parser/smt2perr144.smt2'], ['parser/smt2perr145.smt2'], ['parser/smt2perr146.smt2'], ['parser/smt2perr147.smt2'], ['parser/smt2perr148.smt2'], ['parser/smt2perr149.smt2'], ['parser/smt2perr150.smt2'], ['parser/smt2perr151.smt2'], ['parser/smt2perr152.smt2'], ['parser/smt2perr153.smt2'], ['parser/smt2perr155.smt2'], ['parser/smt2perr156.smt2'], ['parser/smt2perr157.smt2'], ['parser/smt2perr158.smt2'], ['parser/smt2perr159.smt2'], ['parser/smt2perr160.smt2'], ['parser/smt2perr161.smt2'], ['parser/smt2perr162.smt2'], ['parser/smt2perr163.smt2'], ['parser/smt2perr164.smt2'], ['parser/smt2perr165.smt2'], ['parser/smt2perr166.smt2'], ['parser/smt2perr167.smt2'], ['parser/smt2perr168.smt2'], ['parser/smt2perr169.smt2'], ['parser/smt2perr170.smt2'], ['parser/smt2perr171.smt2'], ['parser/smt2perr172.smt2'], ['parser/smt2perr173.smt2'], ['parser/smt2perr174.smt2'], ['parser/smt2perr175.smt2'], ['parser/smt2perr176.smt2'], ['parser/smt2perr177.smt2'], ['parser/smt2perr178.smt2'], ['parser/smt2perr179.smt2'], ['parser/smt2perr180.smt2'], ['parser/smt2perr181.smt2'], ['parser/smt2perr182.smt2'], ['parser/smt2perr183.smt2'], ['parser/smt2perr184.smt2'], ['parser/smt2perr185.smt2'], ['parser/smt2perr186.smt2'], ['parser/smt2perr187.smt2'], ['parser/smt2perr188.smt2'], ['parser/smt2perr189.smt2'], ['parser/smt2perr190.smt2'], ['parser/smt2perr191.smt2'], ['parser/smt2perr192.smt2'], ['parser/smt2perr193.smt2'], ['parser/smt2perr194.smt2'], ['parser/smt2perr195.smt2'], ['parser/smt2perr196.smt2'], ['parser/smt2perr197.smt2'], ['parser/smt2perr198.smt2'], ['parser/smt2perr199.smt2'], ['parser/smt2perr200.smt2'], ['parser/smt2perr201.smt2'], ['parser/smt2perr202.smt2'], ['parser/smt2perr203.smt2'], ['parser/smt2perr204.smt2'], ['parser/smt2perr205.smt2'], ['parser/smt2perr206.smt2'], ['parser/smt2perr207.smt2'], ['parser/smt2perr208.smt2'], ['parser/smt2perr209.smt2'], ['parser/smt2perr210.smt2'], ['parser/smt2perr211.smt2'], ['parser/smt2perr212.smt2'], ['parser/smt2perr213.smt2'], ['parser/smt2perr214.smt2'], #['preprocess/array/nondestr_subst1.smt2'], # TODO slow ['preprocess/array/nondestr_subst10.smt2'], ['preprocess/array/nondestr_subst11.smt2'], ['preprocess/array/nondestr_subst12.smt2'], ['preprocess/array/nondestr_subst13.smt2'], ['preprocess/array/nondestr_subst14.smt2'], ['preprocess/array/nondestr_subst15.smt2'], ['preprocess/array/nondestr_subst16.smt2'], ['preprocess/array/nondestr_subst17.smt2'], ['preprocess/array/nondestr_subst18.smt2'], ['preprocess/array/nondestr_subst19.smt2'], ['preprocess/array/nondestr_subst2.smt2'], ['preprocess/array/nondestr_subst20.smt2'], ['preprocess/array/nondestr_subst3.smt2'], ['preprocess/array/nondestr_subst4.smt2'], ['preprocess/array/nondestr_subst5.smt2'], ['preprocess/array/nondestr_subst6.smt2'], ['preprocess/array/nondestr_subst7.smt2'], ['preprocess/array/nondestr_subst8.smt2'], ['preprocess/array/nondestr_subst9.smt2'], ['preprocess/array/regrembeddedconstraint1.btor.smt2', ['-rwl=0']], ['preprocess/array/regrembeddedconstraint1.btor.smt2', ['-rwl=1']], ['preprocess/array/regrembeddedconstraint1.btor.smt2', ['-rwl=2']], ['preprocess/array/regrembeddedconstraint10.btor.smt2', ['-rwl=0']], ['preprocess/array/regrembeddedconstraint10.btor.smt2', ['-rwl=1']], ['preprocess/array/regrembeddedconstraint10.btor.smt2'], ['preprocess/array/regrembeddedconstraint5.btor.smt2', ['-rwl=0']], ['preprocess/array/regrembeddedconstraint5.btor.smt2', ['-rwl=1']], ['preprocess/array/regrembeddedconstraint5.btor.smt2'], ['preprocess/array/regrembeddedconstraint7.btor.smt2', ['-rwl=0']], ['preprocess/array/regrembeddedconstraint7.btor.smt2', ['-rwl=1']], ['preprocess/array/regrembeddedconstraint7.btor.smt2'], ['preprocess/array/regrembeddedconstraint8.btor.smt2', ['-rwl=0']], ['preprocess/array/regrembeddedconstraint8.btor.smt2', ['-rwl=1']], ['preprocess/array/regrembeddedconstraint8.btor.smt2'], ['preprocess/bv/normaddneg0.btor.smt2'], ['preprocess/bv/normaddneg1.btor.smt2'], ['preprocess/bv/normaddneg2.btor.smt2'], ['preprocess/bv/normaddneg3.btor.smt2'], ['preprocess/bv/normalize-bench_1194.smt2'], ['preprocess/bv/normalize-predicate_961.smt2'], ['preprocess/bv/regrembeddedconstraint11.btor.smt2', ['-rwl=0']], ['preprocess/bv/regrembeddedconstraint11.btor.smt2', ['-rwl=1']], ['preprocess/bv/regrembeddedconstraint11.btor.smt2', ['-rwl=2']], ['preprocess/bv/regrembeddedconstraint14.btor.smt2', ['-rwl=0']], ['preprocess/bv/regrembeddedconstraint14.btor.smt2', ['-rwl=1']], ['preprocess/bv/regrembeddedconstraint14.btor.smt2', ['-rwl=2']], ['preprocess/bv/regrembeddedconstraint3.btor.smt2', ['-rwl=0']], ['preprocess/bv/regrembeddedconstraint3.btor.smt2', ['-rwl=1']], ['preprocess/bv/regrembeddedconstraint3.btor.smt2', ['-rwl=2']], ['preprocess/bv/regrembeddedconstraint9.btor.smt2', ['-rwl=0']], ['preprocess/bv/regrembeddedconstraint9.btor.smt2', ['-rwl=1']], ['preprocess/bv/regrembeddedconstraint9.btor.smt2', ['-rwl=2']], ['preprocess/bv/substcyclic1.btor.smt2'], ['preprocess/bv/substitute1.btor.smt2'], ['preprocess/bv/substitute10.btor.smt2'], ['preprocess/bv/substitute11.btor.smt2'], ['preprocess/bv/substitute12.btor.smt2'], ['preprocess/bv/substitute13.btor.smt2'], ['preprocess/bv/substitute14.btor.smt2'], ['preprocess/bv/substitute15.btor.smt2'], ['preprocess/bv/substitute16.btor.smt2'], ['preprocess/bv/substitute17.btor.smt2'], ['preprocess/bv/substitute18.btor.smt2'], ['preprocess/bv/substitute19.btor.smt2'], ['preprocess/bv/substitute2.btor.smt2'], ['preprocess/bv/substitute20.btor.smt2'], ['preprocess/bv/substitute21.btor.smt2'], ['preprocess/bv/substitute22.btor.smt2'], ['preprocess/bv/substitute23.btor.smt2'], ['preprocess/bv/substitute24.btor.smt2'], ['preprocess/bv/substitute25.btor.smt2'], ['preprocess/bv/substitute26.btor.smt2'], ['preprocess/bv/substitute27.btor.smt2'], ['preprocess/bv/substitute28.btor.smt2'], ['preprocess/bv/substitute29.btor.smt2'], ['preprocess/bv/substitute3.btor.smt2'], ['preprocess/bv/substitute30.btor.smt2'], ['preprocess/bv/substitute31.btor.smt2'], ['preprocess/bv/substitute32.btor.smt2'], ['preprocess/bv/substitute33.btor.smt2'], ['preprocess/bv/substitute34.btor.smt2'], ['preprocess/bv/substitute35.btor.smt2'], ['preprocess/bv/substitute36.btor.smt2'], ['preprocess/bv/substitute36.smt2'], ['preprocess/bv/substitute37.btor.smt2'], ['preprocess/bv/substitute38.btor.smt2'], ['preprocess/bv/substitute39.btor.smt2'], ['preprocess/bv/substitute4.btor.smt2'], ['preprocess/bv/substitute40.btor.smt2'], ['preprocess/bv/substitute5.btor.smt2'], ['preprocess/bv/substitute6.btor.smt2'], ['preprocess/bv/substitute7.btor.smt2'], ['preprocess/bv/substitute8.btor.smt2'], ['preprocess/bv/substitute9.btor.smt2'], ['preprocess/bv/ultsubst1.btor.smt2', ['-rwl=0']], ['preprocess/bv/ultsubst1.btor.smt2', ['-rwl=2']], ['preprocess/bv/ultsubst2.btor.smt2', ['-rwl=0']], ['preprocess/bv/ultsubst2.btor.smt2', ['-rwl=2']], ['preprocess/bv/ultsubst3.btor.smt2', ['-rwl=0']], ['preprocess/bv/ultsubst3.btor.smt2', ['-rwl=2']], ['preprocess/bv/ultsubst4.btor.smt2', ['-rwl=0']], ['preprocess/bv/ultsubst4.btor.smt2', ['-rwl=2']], ['preprocess/bv/ultsubst5.btor.smt2', ['-rwl=0']], ['preprocess/bv/ultsubst5.btor.smt2', ['-rwl=2']], ['preprocess/bv/ultsubst6.btor.smt2', ['-rwl=0']], ['preprocess/bv/ultsubst6.btor.smt2', ['-rwl=2']], ['preprocess/bv/ultsubst7.btor.smt2', ['-rwl=0']], ['preprocess/bv/ultsubst7.btor.smt2', ['-rwl=2']], ['preprocess/bv/ultsubst8.btor.smt2', ['-rwl=0']], ['preprocess/bv/ultsubst8.btor.smt2', ['-rwl=2']], ['preprocess/bv/ultsubst9.btor.smt2', ['-rwl=0']], ['preprocess/bv/ultsubst9.btor.smt2', ['-rwl=2']], ['preprocess/fun/lambda_elim1.smt2'], ['preprocess/fun/lambda_elim2.smt2'], ['preprocess/normalize1.smt2'], ['preprocess/normalize2.smt2'], ['preprocess/normalize3.smt2'], ['preprocess/normalize4.smt2'], ['preprocess/normalize5.smt2'], ['preprocess/normalize6.smt2'], ['preprocess/regrinc1.smt2'], ['preprocess/rewrite1.smt2'], ['preprocess/rewrite2.smt2'], ['preprocess/rewrite3.smt2'], ['preprocess/varsubst1.smt2'], ['preprocess/varsubst2.smt2'], ['preprocess/varsubst3.smt2'], ['preprocess/varsubst4.smt2'], ['preprocess/varsubst5.smt2'], ['preprocess/varsubst6.smt2'], ['preprocess/varsubst7.smt2'], ['preprocess/issue51.smt2'], ['rewrite/array/hang_min_32.smt2'], ['rewrite/array/regr3vl4.btor.smt2'], ['rewrite/array/rw115.btor.smt2', ['-rwl=0']], ['rewrite/array/rw115.btor.smt2', ['-rwl=1']], ['rewrite/array/rw116.btor.smt2', ['-rwl=0']], ['rewrite/array/rw116.btor.smt2', ['-rwl=1']], ['rewrite/array/rw123.btor.smt2', ['-rwl=0']], ['rewrite/array/rw123.btor.smt2', ['-rwl=1']], ['rewrite/array/rw124.btor.smt2', ['-rwl=0']], ['rewrite/array/rw124.btor.smt2', ['-rwl=1']], ['rewrite/array/rw134.btor.smt2', ['-rwl=0']], ['rewrite/array/rw134.btor.smt2'], ['rewrite/array/rw16.btor.smt2', ['-rwl=0']], ['rewrite/array/rw16.btor.smt2', ['-rwl=1']], ['rewrite/array/rw16.btor.smt2'], ['rewrite/array/rw17.btor.smt2', ['-rwl=0']], ['rewrite/array/rw17.btor.smt2', ['-rwl=1']], ['rewrite/array/rw17.btor.smt2'], ['rewrite/array/rw178.btor.smt2'], ['rewrite/array/rw18.btor.smt2', ['-rwl=0']], ['rewrite/array/rw18.btor.smt2', ['-rwl=1']], ['rewrite/array/rw18.btor.smt2'], ['rewrite/array/rw213.smt2'], ['rewrite/array/rw30.btor.smt2', ['-rwl=0']], ['rewrite/array/rw30.btor.smt2', ['-rwl=1']], ['rewrite/array/rw31.btor.smt2', ['-rwl=0']], ['rewrite/array/rw31.btor.smt2', ['-rwl=1']], ['rewrite/array/rw32.btor.smt2', ['-rwl=0']], ['rewrite/array/rw32.btor.smt2', ['-rwl=1']], ['rewrite/array/rw33.btor.smt2', ['-rwl=0']], ['rewrite/array/rw33.btor.smt2', ['-rwl=1']], ['rewrite/array/rw34.btor.smt2', ['-rwl=0']], ['rewrite/array/rw34.btor.smt2', ['-rwl=1']], ['rewrite/array/rw35.btor.smt2', ['-rwl=0']], ['rewrite/array/rw35.btor.smt2', ['-rwl=1']], ['rewrite/array/rw92.btor.smt2', ['-rwl=0']], ['rewrite/array/rw92.btor.smt2', ['-rwl=1']], ['rewrite/array/rw93.btor.smt2', ['-rwl=0']], ['rewrite/array/rw93.btor.smt2', ['-rwl=1']], ['rewrite/array/rwpropindexplusconst1.btor.smt2', ['-rwl=0']], ['rewrite/array/rwpropindexplusconst1.btor.smt2'], ['rewrite/array/rwpropindexplusconst2.btor.smt2', ['-rwl=0']], ['rewrite/array/rwpropindexplusconst2.btor.smt2'], ['rewrite/array/rwpropindexplusconst3.btor.smt2', ['-rwl=0']], ['rewrite/array/rwpropindexplusconst3.btor.smt2'], ['rewrite/array/rwpropindexplusconst4.btor.smt2', ['-rwl=0']], ['rewrite/array/rwpropindexplusconst4.btor.smt2'], ['rewrite/array/rwpropindexpluszero1.btor.smt2', ['-rwl=0']], ['rewrite/array/rwpropindexpluszero1.btor.smt2'], ['rewrite/array/rwpropindexpluszero2.btor.smt2', ['-rwl=0']], ['rewrite/array/rwpropindexpluszero2.btor.smt2'], ['rewrite/array/rwpropindexpluszero3.btor.smt2', ['-rwl=0']], ['rewrite/array/rwpropindexpluszero3.btor.smt2'], ['rewrite/array/rwpropindexpluszero4.btor.smt2', ['-rwl=0']], ['rewrite/array/rwpropindexpluszero4.btor.smt2'], ['rewrite/array/rwpropindexpluszero5.btor.smt2', ['-rwl=0']], ['rewrite/array/rwpropindexpluszero5.btor.smt2'], ['rewrite/array/rwpropindexpluszero6.btor.smt2', ['-rwl=0']], ['rewrite/array/rwpropindexpluszero6.btor.smt2'], ['rewrite/array/rwpropindexpluszero7.btor.smt2', ['-rwl=0']], ['rewrite/array/rwpropindexpluszero7.btor.smt2'], ['rewrite/array/rwpropindexpluszero8.btor.smt2', ['-rwl=0']], ['rewrite/array/rwpropindexpluszero8.btor.smt2'], ['rewrite/array/rww1.btor.smt2'], ['rewrite/bv/3vl2.btor.smt2', ['-rwl=0']], ['rewrite/bv/3vl2.btor.smt2', ['-rwl=2']], ['rewrite/bv/3vl3.btor.smt2', ['-rwl=0']], ['rewrite/bv/3vl3.btor.smt2', ['-rwl=2']], ['rewrite/bv/3vl4.btor.smt2', ['-rwl=0']], ['rewrite/bv/3vl4.btor.smt2', ['-rwl=2']], ['rewrite/bv/3vl5.btor.smt2', ['-rwl=0']], ['rewrite/bv/3vl5.btor.smt2', ['-rwl=2']], ['rewrite/bv/3vl6.btor.smt2', ['-rwl=0']], ['rewrite/bv/3vl6.btor.smt2', ['-rwl=2']], ['rewrite/bv/eq_special_const_bvand.smt2'], ['rewrite/bv/eq_special_const_bvor.smt2'], ['rewrite/bv/rw1.btor.smt2'], ['rewrite/bv/rw10.btor.smt2'], ['rewrite/bv/rw100.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw100.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw101.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw101.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw102.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw102.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw103.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw103.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw104.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw104.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw105.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw105.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw106.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw106.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw107.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw107.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw108.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw108.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw109.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw109.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw11.btor.smt2'], ['rewrite/bv/rw110.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw110.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw111.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw111.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw112.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw112.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw113.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw113.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw114.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw114.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw117.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw117.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw118.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw118.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw119.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw119.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw12.btor.smt2'], ['rewrite/bv/rw120.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw120.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw121.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw121.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw122.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw122.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw125.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw125.btor.smt2'], ['rewrite/bv/rw126.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw126.btor.smt2'], ['rewrite/bv/rw127.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw127.btor.smt2'], ['rewrite/bv/rw128.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw128.btor.smt2'], ['rewrite/bv/rw129.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw129.btor.smt2'], ['rewrite/bv/rw13.btor.smt2'], ['rewrite/bv/rw130.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw130.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw131.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw131.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw132.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw132.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw133.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw133.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw135.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw135.btor.smt2'], ['rewrite/bv/rw136.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw136.btor.smt2'], ['rewrite/bv/rw137.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw137.btor.smt2'], ['rewrite/bv/rw138.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw138.btor.smt2'], ['rewrite/bv/rw139.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw139.btor.smt2'], ['rewrite/bv/rw14.btor.smt2'], ['rewrite/bv/rw140.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw140.btor.smt2'], ['rewrite/bv/rw141.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw141.btor.smt2'], ['rewrite/bv/rw142.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw142.btor.smt2'], ['rewrite/bv/rw143.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw143.btor.smt2'], ['rewrite/bv/rw144.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw144.btor.smt2'], ['rewrite/bv/rw145.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw145.btor.smt2'], ['rewrite/bv/rw146.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw146.btor.smt2'], ['rewrite/bv/rw147.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw147.btor.smt2'], ['rewrite/bv/rw148.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw148.btor.smt2'], ['rewrite/bv/rw149.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw149.btor.smt2'], ['rewrite/bv/rw15.btor.smt2'], ['rewrite/bv/rw150.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw150.btor.smt2'], ['rewrite/bv/rw151.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw151.btor.smt2'], ['rewrite/bv/rw152.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw152.btor.smt2'], ['rewrite/bv/rw153.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw153.btor.smt2'], ['rewrite/bv/rw154.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw154.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw155.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw155.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw156.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw156.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw157.btor.smt2'], ['rewrite/bv/rw158.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw159.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw160.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw161.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw162.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw163.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw164.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw165.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw166.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw167.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw168.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw169.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw170.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw171.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw172.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw173.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw174.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw175.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw176.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw177.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw179.btor.smt2'], ['rewrite/bv/rw180.btor.smt2'], ['rewrite/bv/rw181.btor.smt2'], ['rewrite/bv/rw182.btor.smt2'], ['rewrite/bv/rw183.btor.smt2'], ['rewrite/bv/rw184.btor.smt2'], ['rewrite/bv/rw185.btor.smt2'], ['rewrite/bv/rw186.btor.smt2'], ['rewrite/bv/rw187.btor.smt2'], ['rewrite/bv/rw188.btor.smt2'], ['rewrite/bv/rw189.btor.smt2'], ['rewrite/bv/rw19.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw19.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw190.btor.smt2'], ['rewrite/bv/rw191.btor.smt2'], ['rewrite/bv/rw192.btor.smt2'], ['rewrite/bv/rw193.btor.smt2'], ['rewrite/bv/rw194.btor.smt2'], ['rewrite/bv/rw195.btor.smt2'], ['rewrite/bv/rw196.btor.smt2'], ['rewrite/bv/rw197.btor.smt2'], ['rewrite/bv/rw198.btor.smt2'], ['rewrite/bv/rw199.btor.smt2'], ['rewrite/bv/rw2.btor.smt2'], ['rewrite/bv/rw20.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw20.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw200.btor.smt2'], ['rewrite/bv/rw201.btor.smt2'], ['rewrite/bv/rw202.btor.smt2'], ['rewrite/bv/rw203.btor.smt2'], ['rewrite/bv/rw204.btor.smt2'], ['rewrite/bv/rw205.btor.smt2'], ['rewrite/bv/rw206.btor.smt2'], ['rewrite/bv/rw207.btor.smt2'], ['rewrite/bv/rw208.btor.smt2'], ['rewrite/bv/rw209.btor.smt2'], ['rewrite/bv/rw21.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw21.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw210.btor.smt2'], ['rewrite/bv/rw211.btor.smt2'], ['rewrite/bv/rw212.smt2'], ['rewrite/bv/rw214.smt2'], ['rewrite/bv/rw215.smt2'], ['rewrite/bv/rw216.smt2'], ['rewrite/bv/rw217.smt2'], ['rewrite/bv/rw218.smt2'], ['rewrite/bv/rw219.smt2'], ['rewrite/bv/rw22.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw22.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw220.smt2'], ['rewrite/bv/rw221.smt2'], ['rewrite/bv/rw23.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw23.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw24.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw24.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw25.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw25.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw26.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw26.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw27.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw27.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw28.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw28.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw29.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw29.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw3.btor.smt2'], ['rewrite/bv/rw36.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw36.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw37.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw37.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw38.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw38.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw39.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw39.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw4.btor.smt2'], ['rewrite/bv/rw40.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw40.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw41.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw41.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw42.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw42.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw43.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw43.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw44.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw44.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw45.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw45.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw46.btor.smt2'], ['rewrite/bv/rw47.btor.smt2'], #['rewrite/bv/rw48.btor.smt2'], # TODO too slow (32s) #['rewrite/bv/rw49.btor.smt2'], # TODO too slow (145s) ['rewrite/bv/rw5.btor.smt2'], #['rewrite/bv/rw50.btor.smt2'], # TODO too slow (timeout after 150s) ['rewrite/bv/rw51.btor.smt2'], ['rewrite/bv/rw52.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw52.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw53.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw53.btor.smt2'], ['rewrite/bv/rw54.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw54.btor.smt2'], ['rewrite/bv/rw55.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw55.btor.smt2'], ['rewrite/bv/rw56.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw56.btor.smt2'], ['rewrite/bv/rw57.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw57.btor.smt2'], ['rewrite/bv/rw58.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw58.btor.smt2'], ['rewrite/bv/rw59.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw59.btor.smt2'], ['rewrite/bv/rw6.btor.smt2'], #['rewrite/bv/rw60.btor.smt2'], # TODO too slow (timeout after 150s) ['rewrite/bv/rw61.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw61.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw62.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw62.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw63.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw63.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw64.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw64.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw65.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw65.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw66.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw66.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw67.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw67.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw68.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw68.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw69.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw69.btor.smt2'], ['rewrite/bv/rw7.btor.smt2'], ['rewrite/bv/rw70.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw70.btor.smt2'], ['rewrite/bv/rw71.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw71.btor.smt2'], ['rewrite/bv/rw72.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw72.btor.smt2'], ['rewrite/bv/rw73.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw73.btor.smt2'], ['rewrite/bv/rw74.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw74.btor.smt2'], ['rewrite/bv/rw75.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw75.btor.smt2'], ['rewrite/bv/rw76.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw76.btor.smt2'], ['rewrite/bv/rw77.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw77.btor.smt2'], ['rewrite/bv/rw78.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw78.btor.smt2'], ['rewrite/bv/rw79.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw79.btor.smt2'], ['rewrite/bv/rw8.btor.smt2'], ['rewrite/bv/rw80.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw80.btor.smt2'], ['rewrite/bv/rw81.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw81.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw82.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw82.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw83.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw83.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw84.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw84.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw85.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw85.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw86.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw86.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw87.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw87.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw88.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw88.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw89.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw89.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw9.btor.smt2'], ['rewrite/bv/rw90.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw90.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw91.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw91.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw94.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw94.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw95.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw95.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw96.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw96.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw97.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw97.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw98.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw98.btor.smt2', ['-rwl=1']], ['rewrite/bv/rw99.btor.smt2', ['-rwl=0']], ['rewrite/bv/rw99.btor.smt2', ['-rwl=1']], #['solver/declsort0.smt2'], # TODO: disabled due to missing support in fun solver #['solver/declsort1.smt2'], # TODO: disabled due to missing support in fun solver ['solver/array/arraycond1.btor.smt2'], ['solver/array/arraycond10.btor.smt2'], ['solver/array/arraycond11.btor.smt2'], ['solver/array/arraycond12.btor.smt2'], ['solver/array/arraycond13.btor.smt2'], ['solver/array/arraycond14.btor.smt2'], ['solver/array/arraycond15.btor.smt2'], ['solver/array/arraycond16.btor.smt2'], ['solver/array/arraycond17.btor.smt2'], ['solver/array/arraycond18.btor.smt2'], ['solver/array/arraycond2.btor.smt2'], ['solver/array/arraycond3.btor.smt2'], ['solver/array/arraycond4.btor.smt2'], ['solver/array/arraycond5.btor.smt2'], ['solver/array/arraycond6.btor.smt2'], ['solver/array/arraycond7.btor.smt2'], ['solver/array/arraycond8.btor.smt2'], ['solver/array/arraycond9.btor.smt2'], ['solver/array/arraycondconst.btor.smt2', ['-rwl=0']], ['solver/array/arraycondconstaig.btor.smt2', ['-rwl=0']], ['solver/array/binarysearch32s016.smt2'], ['solver/array/bubsort002un.smt2'], ['solver/array/computeparents.smt2', ['--bv-solver=prop']], ['solver/array/computeparents.smt2'], ['solver/array/constarray.smt2'], ['solver/array/dubreva002ue.smt2'], ['solver/array/duplicatelemma1.smt2'], ['solver/array/duplicatelemma2.smt2'], #['solver/array/duplicatelemma3.smt2'], # TODO: disabled because of equality over constant arrays ['solver/array/ext1.btor.smt2'], ['solver/array/ext10.btor.smt2'], ['solver/array/ext11.btor.smt2'], ['solver/array/ext12.btor.smt2'], ['solver/array/ext13.btor.smt2'], ['solver/array/ext14.btor.smt2'], ['solver/array/ext15.btor.smt2'], ['solver/array/ext16.btor.smt2'], ['solver/array/ext17.btor.smt2'], ['solver/array/ext18.btor.smt2'], ['solver/array/ext19.btor.smt2'], ['solver/array/ext2.btor.smt2'], ['solver/array/ext20.btor.smt2'], ['solver/array/ext21.btor.smt2'], ['solver/array/ext22.btor.smt2'], ['solver/array/ext23.btor.smt2'], ['solver/array/ext24.btor.smt2'], ['solver/array/ext25.btor.smt2'], ['solver/array/ext26.btor.smt2'], ['solver/array/ext27.btor.smt2'], ['solver/array/ext28.btor.smt2'], ['solver/array/ext29.btor.smt2'], ['solver/array/ext3.btor.smt2'], ['solver/array/ext4.btor.smt2'], ['solver/array/ext5.btor.smt2'], ['solver/array/ext6.btor.smt2'], ['solver/array/ext7.btor.smt2'], ['solver/array/ext8.btor.smt2'], ['solver/array/ext9.btor.smt2'], ['solver/array/extarraywrite1.btor.smt2'], ['solver/array/extarraywrite2.btor.smt2'], ['solver/array/extarraywrite3.smt2'], ['solver/array/extarraywrite3sat.smt2'], ['solver/array/fifo32bc04k05.smt2'], ['solver/array/fifo32ia04k05.smt2'], ['solver/array/fifo32in04k05.smt2'], ['solver/array/invalidmodel1.smt2'], #['solver/array/invalidmodel2.smt2', ['-xl=0 -ml=0 -rwl=2']], # TODO: disabled because of options ['solver/array/invalidmodel3.btor.smt2'], ['solver/array/issue32.smt2'], ['solver/array/issue35.smt2'], ['solver/array/lazyreadwritebug1.btor.smt2'], ['solver/array/memcpy02.smt2'], ['solver/array/random1.btor.smt2'], ['solver/array/random2.btor.smt2'], ['solver/array/random3.btor.smt2'], ['solver/array/read1.btor.smt2'], ['solver/array/read10.btor.smt2'], ['solver/array/read11.btor.smt2'], ['solver/array/read12.btor.smt2'], ['solver/array/read13.btor.smt2'], ['solver/array/read14.btor.smt2'], ['solver/array/read15.btor.smt2'], ['solver/array/read16.btor.smt2'], ['solver/array/read17.btor.smt2'], ['solver/array/read18.btor.smt2'], ['solver/array/read19.btor.smt2'], ['solver/array/read2.btor.smt2'], ['solver/array/read20.btor.smt2'], ['solver/array/read21.btor.smt2'], ['solver/array/read22.btor.smt2'], ['solver/array/read3.btor.smt2'], ['solver/array/read4.btor.smt2'], ['solver/array/read5.btor.smt2'], ['solver/array/read6.btor.smt2'], ['solver/array/read7.btor.smt2'], ['solver/array/read8.btor.smt2'], ['solver/array/read9.btor.smt2'], ['solver/array/regprim11simp.btor.smt2'], ['solver/array/regrarray1.smt2'], ['solver/array/regrarray10.smt2'], ['solver/array/regrarray11.smt2'], ['solver/array/regrarray2.smt2'], ['solver/array/regrarray3.smt2'], ['solver/array/regrarray4.smt2'], ['solver/array/regrarray5.smt2'], ['solver/array/regrarray6.smt2'], ['solver/array/regrarray7.smt2'], ['solver/array/regrarray8.smt2'], ['solver/array/regrarray9.smt2'], ['solver/array/regrbetacache1.btor.smt2'], ['solver/array/selsort002un.smt2'], ['solver/array/smtarraycond1.smt2'], ['solver/array/smtarraycond2.smt2'], ['solver/array/smtarraycond3.smt2'], ['solver/array/smtaxiommccarthy.smt2'], ['solver/array/smtextarray1sat0.smt2'], ['solver/array/smtextarray1sat1.smt2'], ['solver/array/smtextarray2sat0.smt2'], ['solver/array/smtextarray2sat1.smt2'], ['solver/array/smtextarray2sat2.smt2'], ['solver/array/smtextarray2sat3.smt2'], ['solver/array/smtextarray3sat0.smt2'], ['solver/array/smtextarray3sat1.smt2'], ['solver/array/smtextarray3sat2.smt2'], ['solver/array/smtextarray3sat3.smt2'], ['solver/array/smtextarray3sat4.smt2'], ['solver/array/smtextarray3sat5.smt2'], ['solver/array/smtextarray3sat6.smt2'], ['solver/array/smtextarray3sat7.smt2'], ['solver/array/smtextarrayaxiom1.smt2'], ['solver/array/smtextarrayaxiom1uf.smt2'], ['solver/array/smtextarrayaxiom2.smt2'], ['solver/array/smtextarrayaxiom2uf.smt2'], ['solver/array/smtextarrayaxiom3.smt2'], ['solver/array/smtextarrayaxiom3uf.smt2'], ['solver/array/smtextarrayaxiom4.smt2'], ['solver/array/smtextarrayaxiom4uf.smt2'], ['solver/array/swapmem002se.smt2'], ['solver/array/swapmem002ue.smt2'], ['solver/array/upprop1.btor.smt2'], ['solver/array/wchains002se.smt2'], ['solver/array/wchains002ue.smt2'], ['solver/array/write1.btor.smt2'], ['solver/array/write10.btor.smt2'], ['solver/array/write11.btor.smt2'], ['solver/array/write12.btor.smt2'], ['solver/array/write13.btor.smt2'], ['solver/array/write14.btor.smt2'], ['solver/array/write15.btor.smt2'], ['solver/array/write16.btor.smt2'], ['solver/array/write17.btor.smt2'], ['solver/array/write18.btor.smt2'], ['solver/array/write19.btor.smt2'], ['solver/array/write2.btor.smt2'], ['solver/array/write20.btor.smt2'], ['solver/array/write21.btor.smt2'], ['solver/array/write22.btor.smt2'], ['solver/array/write23.btor.smt2'], ['solver/array/write24.btor.smt2'], ['solver/array/write3.btor.smt2'], ['solver/array/write4.btor.smt2'], ['solver/array/write5.btor.smt2'], ['solver/array/write6.btor.smt2'], ['solver/array/write7.btor.smt2'], ['solver/array/write8.btor.smt2'], ['solver/array/write9.btor.smt2'], ['solver/bv/addnegmul1.btor.smt2'], ['solver/bv/andopt1.btor.smt2'], ['solver/bv/andopt10.btor.smt2'], ['solver/bv/andopt11.btor.smt2'], ['solver/bv/andopt12.btor.smt2'], ['solver/bv/andopt13.btor.smt2'], ['solver/bv/andopt14.btor.smt2'], ['solver/bv/andopt15.btor.smt2'], ['solver/bv/andopt16.btor.smt2'], ['solver/bv/andopt17.btor.smt2'], ['solver/bv/andopt2.btor.smt2'], ['solver/bv/andopt3.btor.smt2'], ['solver/bv/andopt4.btor.smt2'], ['solver/bv/andopt5.btor.smt2'], ['solver/bv/andopt6.btor.smt2'], ['solver/bv/andopt7.btor.smt2'], ['solver/bv/andopt8.btor.smt2'], ['solver/bv/andopt9.btor.smt2'], ['solver/bv/const1.btor.smt2'], ['solver/bv/const2.btor.smt2'], ['solver/bv/countbits016.smt2'], ['solver/bv/dec_rwl0.btor.smt2', ['-rwl=0']], ['solver/bv/dec_rwl3.btor.smt2'], ['solver/bv/distri1.btor.smt2'], ['solver/bv/distri2.btor.smt2'], ['solver/bv/distri3.btor.smt2'], ['solver/bv/distri4.btor.smt2'], ['solver/bv/distri5.btor.smt2'], ['solver/bv/distri6.btor.smt2'], ['solver/bv/distri7.btor.smt2'], ['solver/bv/distri8.btor.smt2'], ['solver/bv/exactlyone.btor.smt2'], ['solver/bv/factor18446744073709551617const.btor.smt2'], ['solver/bv/factor18446744073709551617xconst.btor.smt2'], ['solver/bv/factor18446744073709551617yconst.btor.smt2'], ['solver/bv/factor2209.btor.smt2'], ['solver/bv/factor4294967295.btor.smt2'], ['solver/bv/factor4294967297.btor.smt2'], ['solver/bv/hd1.btor.smt2', ['-rwl=0']], ['solver/bv/hd1.btor.smt2', ['-rwl=1']], ['solver/bv/hd10.btor.smt2', ['-rwl=0']], ['solver/bv/hd10.btor.smt2', ['-rwl=1']], ['solver/bv/hd11.btor.smt2', ['-rwl=0']], ['solver/bv/hd11.btor.smt2', ['-rwl=1']], ['solver/bv/hd12.btor.smt2', ['-rwl=0']], ['solver/bv/hd12.btor.smt2', ['-rwl=1']], ['solver/bv/hd13.btor.smt2', ['-rwl=0']], ['solver/bv/hd13.btor.smt2', ['-rwl=1']], ['solver/bv/hd14.btor.smt2', ['-rwl=0']], ['solver/bv/hd14.btor.smt2', ['-rwl=1']], ['solver/bv/hd15.btor.smt2', ['-rwl=0']], ['solver/bv/hd15.btor.smt2', ['-rwl=1']], ['solver/bv/hd16.btor.smt2', ['-rwl=0']], ['solver/bv/hd16.btor.smt2', ['-rwl=1']], ['solver/bv/hd17.btor.smt2', ['-rwl=0']], ['solver/bv/hd17.btor.smt2', ['-rwl=1']], ['solver/bv/hd18.btor.smt2', ['-rwl=0']], ['solver/bv/hd18.btor.smt2', ['-rwl=1']], ['solver/bv/hd19.btor.smt2'], ['solver/bv/hd2.btor.smt2', ['-rwl=0']], ['solver/bv/hd2.btor.smt2', ['-rwl=1']], ['solver/bv/hd20.btor.smt2'], ['solver/bv/hd21.btor.smt2'], ['solver/bv/hd3.btor.smt2', ['-rwl=0']], ['solver/bv/hd3.btor.smt2', ['-rwl=1']], ['solver/bv/hd4.btor.smt2', ['-rwl=0']], ['solver/bv/hd4.btor.smt2', ['-rwl=1']], ['solver/bv/hd5.btor.smt2', ['-rwl=0']], ['solver/bv/hd5.btor.smt2', ['-rwl=1']], ['solver/bv/hd6.btor.smt2', ['-rwl=0']], ['solver/bv/hd6.btor.smt2', ['-rwl=1']], ['solver/bv/hd7.btor.smt2', ['-rwl=0']], ['solver/bv/hd7.btor.smt2', ['-rwl=1']], ['solver/bv/hd8.btor.smt2', ['-rwl=0']], ['solver/bv/hd8.btor.smt2', ['-rwl=1']], ['solver/bv/hd9.btor.smt2', ['-rwl=0']], ['solver/bv/hd9.btor.smt2', ['-rwl=1']], ['solver/bv/inc.btor.smt2', ['-rwl=0']], ['solver/bv/inc.btor.smt2'], ['solver/bv/lin0.btor.smt2'], ['solver/bv/lin1.btor.smt2'], ['solver/bv/lin2.btor.smt2'], ['solver/bv/lin3.btor.smt2'], ['solver/bv/lin4.btor.smt2'], ['solver/bv/mulassoc4.smt2'], ['solver/bv/mulassoc5.smt2'], ['solver/bv/mulassoc6.smt2'], ['solver/bv/nextpoweroftwo016.smt2'], ['solver/bv/painc.smt2'], ['solver/bv/preprop1.smt2'], ['solver/bv/prim8bugreduced.btor.smt2'], ['solver/bv/problem_130.smt2'], ['solver/bv/prop/prels-funs.smt2', ['--bv-solver=preprop']], ['solver/bv/prop/prop_essential_checks_cycle.smt2', ['--bv-solver=prop --prop-sext --prop-ineq-bounds']], # --prop-use-inv-lt-concat" # TODO option currently disabled ['solver/bv/prop/prop_fp.smt2', ['--bv-solver=prop']], ['solver/bv/prop/prop_fp_inc.smt2', ['--bv-solver=prop']], ['solver/bv/prop/prop_ineq_bounds_cycle.smt2', ['--bv-solver=prop --prop-sext --prop-ineq-bounds']], # --prop-use-inv-lt-concat" # TODO option currently disabled ['solver/bv/prop/prop_not_sat.smt2', ['--bv-solver=prop --prop-nprops=10000 --prop-nupdates=2000000']], ['solver/bv/prop/prop_top_level_const_bits.smt2', ['--bv-solver=preprop']], ['solver/bv/prop/prop_wheel_factorizer.smt2', ['--bv-solver=prop']], ['solver/bv/proxybug.btor.smt2'], ['solver/bv/redand3twice.btor.smt2'], ['solver/bv/redand3twice.smt2'], ['solver/bv/redor3.btor.smt2'], ['solver/bv/regr-5smod3.btor.smt2'], ['solver/bv/regr-5srem3.btor.smt2'], ['solver/bv/regr-6smod3.btor.smt2'], ['solver/bv/regr-6srem3.btor.smt2'], ['solver/bv/regr5smod-3.btor.smt2'], ['solver/bv/regr5srem-3.btor.smt2'], ['solver/bv/regr6smod-3.btor.smt2'], ['solver/bv/regr6srem-3.btor.smt2'], ['solver/bv/regrcalypto1.smt2'], ['solver/bv/regrcalypto2.smt2'], ['solver/bv/regrcalypto3.smt2'], ['solver/bv/regrdistinct.smt2'], ['solver/bv/regrdomabst3.btor.smt2'], ['solver/bv/regrdomabst4.btor.smt2'], ['solver/bv/regrexpleak1.btor.smt2', ['-rwl=0']], ['solver/bv/regrexpleak1.btor.smt2', ['-rwl=1']], ['solver/bv/regrexpleak1.btor.smt2', ['-rwl=2']], ['solver/bv/regrmark1.btor.smt2', ['-rwl=0']], ['solver/bv/regrmark1.btor.smt2', ['-rwl=1']], ['solver/bv/regrmark1.btor.smt2', ['-rwl=2']], ['solver/bv/regrpointerchasing1.btor.smt2'], ['solver/bv/regrrwbinexpconcatzeroconst.btor.smt2'], ['solver/bv/regrw8simp.btor.smt2'], ['solver/bv/regsmod1.smt2'], ['solver/bv/regsubslapd149921red.btor.smt2'], ['solver/bv/nego1.smt2'], ['solver/bv/nego2.smt2'], ['solver/bv/saddo1.smt2'], ['solver/bv/saddo2.smt2'], ['solver/bv/sc12fuzzcheck2.smt2'], ['solver/bv/sdivo1.smt2'], ['solver/bv/sdivo2.smt2'], ['solver/bv/slicesubst1.btor.smt2', ['-rwl=0']], ['solver/bv/slicesubst1.btor.smt2', ['-rwl=2']], ['solver/bv/sll_same_bw.btor.smt2'], ['solver/bv/smt2pushpop0.smt2', ['--bv-solver=prop']], ['solver/bv/smt2pushpop0.smt2'], ['solver/bv/smtandvar.smt2'], ['solver/bv/smtashr1.smt2'], ['solver/bv/smtashr2.smt2'], ['solver/bv/smtashr3.smt2'], ['solver/bv/smtaxiombvashr1.smt2'], ['solver/bv/smtaxiombvashr16.smt2'], ['solver/bv/smtaxiombvashr2.smt2'], ['solver/bv/smtaxiombvashr3.smt2'], ['solver/bv/smtaxiombvashr32.smt2'], ['solver/bv/smtaxiombvashr4.smt2'], ['solver/bv/smtaxiombvashr5.smt2'], ['solver/bv/smtaxiombvashr6.smt2'], ['solver/bv/smtaxiombvashr64.smt2'], ['solver/bv/smtaxiombvashr7.smt2'], ['solver/bv/smtaxiombvashr8.smt2'], ['solver/bv/smtaxiombvnand1.smt2'], ['solver/bv/smtaxiombvnand16.smt2'], ['solver/bv/smtaxiombvnand2.smt2'], ['solver/bv/smtaxiombvnand3.smt2'], ['solver/bv/smtaxiombvnand32.smt2'], ['solver/bv/smtaxiombvnand4.smt2'], ['solver/bv/smtaxiombvnand5.smt2'], ['solver/bv/smtaxiombvnand6.smt2'], ['solver/bv/smtaxiombvnand64.smt2'], ['solver/bv/smtaxiombvnand7.smt2'], ['solver/bv/smtaxiombvnand8.smt2'], ['solver/bv/smtaxiombvnor1.smt2'], ['solver/bv/smtaxiombvnor16.smt2'], ['solver/bv/smtaxiombvnor2.smt2'], ['solver/bv/smtaxiombvnor3.smt2'], ['solver/bv/smtaxiombvnor32.smt2'], ['solver/bv/smtaxiombvnor4.smt2'], ['solver/bv/smtaxiombvnor5.smt2'], ['solver/bv/smtaxiombvnor6.smt2'], ['solver/bv/smtaxiombvnor64.smt2'], ['solver/bv/smtaxiombvnor7.smt2'], ['solver/bv/smtaxiombvnor8.smt2'], ['solver/bv/smtaxiombvsdiv1.smt2'], ['solver/bv/smtaxiombvsdiv2.smt2'], ['solver/bv/smtaxiombvsdiv3.smt2'], ['solver/bv/smtaxiombvsdiv4.smt2'], ['solver/bv/smtaxiombvsdiv5.smt2'], ['solver/bv/smtaxiombvsdiv6.smt2'], ['solver/bv/smtaxiombvsdiv7.smt2'], ['solver/bv/smtaxiombvsdiv8.smt2'], #['solver/bv/smtaxiombvsdiv16.smt2'], # hard (slow) #['solver/bv/smtaxiombvsdiv32.smt2'], # hard (slow) #['solver/bv/smtaxiombvsdiv64.smt2'], # hard (slow) ['solver/bv/smtaxiombvsge1.smt2'], ['solver/bv/smtaxiombvsge16.smt2'], ['solver/bv/smtaxiombvsge2.smt2'], ['solver/bv/smtaxiombvsge3.smt2'], ['solver/bv/smtaxiombvsge32.smt2'], ['solver/bv/smtaxiombvsge4.smt2'], ['solver/bv/smtaxiombvsge5.smt2'], ['solver/bv/smtaxiombvsge6.smt2'], ['solver/bv/smtaxiombvsge64.smt2'], ['solver/bv/smtaxiombvsge7.smt2'], ['solver/bv/smtaxiombvsge8.smt2'], ['solver/bv/smtaxiombvsgt1.smt2'], ['solver/bv/smtaxiombvsgt16.smt2'], ['solver/bv/smtaxiombvsgt2.smt2'], ['solver/bv/smtaxiombvsgt3.smt2'], ['solver/bv/smtaxiombvsgt32.smt2'], ['solver/bv/smtaxiombvsgt4.smt2'], ['solver/bv/smtaxiombvsgt5.smt2'], ['solver/bv/smtaxiombvsgt6.smt2'], ['solver/bv/smtaxiombvsgt64.smt2'], ['solver/bv/smtaxiombvsgt7.smt2'], ['solver/bv/smtaxiombvsgt8.smt2'], ['solver/bv/smtaxiombvsle1.smt2'], ['solver/bv/smtaxiombvsle16.smt2'], ['solver/bv/smtaxiombvsle2.smt2'], ['solver/bv/smtaxiombvsle3.smt2'], ['solver/bv/smtaxiombvsle32.smt2'], ['solver/bv/smtaxiombvsle4.smt2'], ['solver/bv/smtaxiombvsle5.smt2'], ['solver/bv/smtaxiombvsle6.smt2'], ['solver/bv/smtaxiombvsle64.smt2'], ['solver/bv/smtaxiombvsle7.smt2'], ['solver/bv/smtaxiombvsle8.smt2'], ['solver/bv/smtaxiombvslt1.smt2'], ['solver/bv/smtaxiombvslt16.smt2'], ['solver/bv/smtaxiombvslt2.smt2'], ['solver/bv/smtaxiombvslt3.smt2'], ['solver/bv/smtaxiombvslt32.smt2'], ['solver/bv/smtaxiombvslt4.smt2'], ['solver/bv/smtaxiombvslt5.smt2'], ['solver/bv/smtaxiombvslt6.smt2'], ['solver/bv/smtaxiombvslt64.smt2'], ['solver/bv/smtaxiombvslt7.smt2'], ['solver/bv/smtaxiombvslt8.smt2'], ['solver/bv/smtaxiombvsmod1.smt2'], ['solver/bv/smtaxiombvsmod2.smt2'], ['solver/bv/smtaxiombvsmod3.smt2'], ['solver/bv/smtaxiombvsmod4.smt2'], ['solver/bv/smtaxiombvsmod5.smt2'], ['solver/bv/smtaxiombvsmod6.smt2'], ['solver/bv/smtaxiombvsmod7.smt2'], ['solver/bv/smtaxiombvsmod8.smt2'], #['solver/bv/smtaxiombvsmod16.smt2'], # hard (slow) #['solver/bv/smtaxiombvsmod32.smt2'], # hard (slow) #['solver/bv/smtaxiombvsmod64.smt2'], # hard (slow) ['solver/bv/smtaxiombvsrem1.smt2'], ['solver/bv/smtaxiombvsrem2.smt2'], ['solver/bv/smtaxiombvsrem3.smt2'], ['solver/bv/smtaxiombvsrem4.smt2'], ['solver/bv/smtaxiombvsrem5.smt2'], ['solver/bv/smtaxiombvsrem6.smt2'], ['solver/bv/smtaxiombvsrem7.smt2'], ['solver/bv/smtaxiombvsrem8.smt2'], #['solver/bv/smtaxiombvsrem16.smt2'], # hard (slow) #['solver/bv/smtaxiombvsrem32.smt2'], # hard (slow) #['solver/bv/smtaxiombvsrem64.smt2'], # hard (slow) ['solver/bv/smtaxiombvsub1.smt2'], ['solver/bv/smtaxiombvsub16.smt2'], ['solver/bv/smtaxiombvsub2.smt2'], ['solver/bv/smtaxiombvsub3.smt2'], ['solver/bv/smtaxiombvsub32.smt2'], ['solver/bv/smtaxiombvsub4.smt2'], ['solver/bv/smtaxiombvsub5.smt2'], ['solver/bv/smtaxiombvsub6.smt2'], ['solver/bv/smtaxiombvsub64.smt2'], ['solver/bv/smtaxiombvsub7.smt2'], ['solver/bv/smtaxiombvsub8.smt2'], ['solver/bv/smtaxiombvuge1.smt2'], ['solver/bv/smtaxiombvuge16.smt2'], ['solver/bv/smtaxiombvuge2.smt2'], ['solver/bv/smtaxiombvuge3.smt2'], ['solver/bv/smtaxiombvuge32.smt2'], ['solver/bv/smtaxiombvuge4.smt2'], ['solver/bv/smtaxiombvuge5.smt2'], ['solver/bv/smtaxiombvuge6.smt2'], ['solver/bv/smtaxiombvuge64.smt2'], ['solver/bv/smtaxiombvuge7.smt2'], ['solver/bv/smtaxiombvuge8.smt2'], ['solver/bv/smtaxiombvugt1.smt2'], ['solver/bv/smtaxiombvugt16.smt2'], ['solver/bv/smtaxiombvugt2.smt2'], ['solver/bv/smtaxiombvugt3.smt2'], ['solver/bv/smtaxiombvugt32.smt2'], ['solver/bv/smtaxiombvugt4.smt2'], ['solver/bv/smtaxiombvugt5.smt2'], ['solver/bv/smtaxiombvugt6.smt2'], ['solver/bv/smtaxiombvugt64.smt2'], ['solver/bv/smtaxiombvugt7.smt2'], ['solver/bv/smtaxiombvugt8.smt2'], ['solver/bv/smtaxiombvule1.smt2'], ['solver/bv/smtaxiombvule16.smt2'], ['solver/bv/smtaxiombvule2.smt2'], ['solver/bv/smtaxiombvule3.smt2'], ['solver/bv/smtaxiombvule32.smt2'], ['solver/bv/smtaxiombvule4.smt2'], ['solver/bv/smtaxiombvule5.smt2'], ['solver/bv/smtaxiombvule6.smt2'], ['solver/bv/smtaxiombvule64.smt2'], ['solver/bv/smtaxiombvule7.smt2'], ['solver/bv/smtaxiombvule8.smt2'], ['solver/bv/smtaxiombvxnor1.smt2'], ['solver/bv/smtaxiombvxnor16.smt2'], ['solver/bv/smtaxiombvxnor2.smt2'], ['solver/bv/smtaxiombvxnor3.smt2'], ['solver/bv/smtaxiombvxnor32.smt2'], ['solver/bv/smtaxiombvxnor4.smt2'], ['solver/bv/smtaxiombvxnor5.smt2'], ['solver/bv/smtaxiombvxnor6.smt2'], ['solver/bv/smtaxiombvxnor64.smt2'], ['solver/bv/smtaxiombvxnor7.smt2'], ['solver/bv/smtaxiombvxnor8.smt2'], ['solver/bv/smtaxiombvxor1.smt2'], ['solver/bv/smtaxiombvxor16.smt2'], ['solver/bv/smtaxiombvxor2.smt2'], ['solver/bv/smtaxiombvxor3.smt2'], ['solver/bv/smtaxiombvxor32.smt2'], ['solver/bv/smtaxiombvxor4.smt2'], ['solver/bv/smtaxiombvxor5.smt2'], ['solver/bv/smtaxiombvxor6.smt2'], ['solver/bv/smtaxiombvxor64.smt2'], ['solver/bv/smtaxiombvxor7.smt2'], ['solver/bv/smtaxiombvxor8.smt2'], ['solver/bv/smtbv255.smt2'], ['solver/bv/smtfalse.smt2'], ['solver/bv/smtflet.smt2'], ['solver/bv/smtiff.smt2'], ['solver/bv/smtlshr1.smt2'], ['solver/bv/smtlshr2.smt2'], ['solver/bv/smtlshr3.smt2'], ['solver/bv/smtnotvar.smt2'], ['solver/bv/smtor.smt2'], ['solver/bv/smtrepeat.smt2'], ['solver/bv/smtrotate.smt2'], ['solver/bv/smtshl1.smt2'], ['solver/bv/smtshl2.smt2'], ['solver/bv/smtshl3.smt2'], ['solver/bv/smtsignextend.smt2'], ['solver/bv/smttrue.smt2'], ['solver/bv/smtvar.smt2'], ['solver/bv/smtxor.smt2'], ['solver/bv/smtzeroextend.smt2'], ['solver/bv/smulo1.smt2'], ['solver/bv/smulo2.smt2'], ['solver/bv/sqrt13.btor.smt2'], ['solver/bv/sqrt18446744073709551617.btor.smt2'], ['solver/bv/sqrt25.btor.smt2'], ['solver/bv/sqrt29.btor.smt2'], ['solver/bv/sqrt31.btor.smt2'], ['solver/bv/sqrt4.btor.smt2'], ['solver/bv/sqrt4294967297.btor.smt2'], ['solver/bv/sqrt4295098369.btor.smt2'], ['solver/bv/sqrt49.btor.smt2'], ['solver/bv/sqrt5.btor.smt2'], ['solver/bv/sqrt65537.btor.smt2'], ['solver/bv/sqrt7.btor.smt2'], ['solver/bv/sqrt9.btor.smt2'], ['solver/bv/srl_same_bw.btor.smt2'], ['solver/bv/ssubo1.smt2'], ['solver/bv/ssubo2.smt2'], ['solver/bv/sult.btor.smt2'], ['solver/bv/sult2.btor.smt2'], ['solver/bv/twocomplementassub.btor.smt2'], ['solver/bv/uaddo1.smt2'], ['solver/bv/uaddo2.smt2'], ['solver/bv/udiv16castdown8.btor.smt2'], ['solver/bv/udiv8castdown4.btor.smt2'], ['solver/bv/udiv8castdown5.btor.smt2'], ['solver/bv/udiv8castdown6.btor.smt2'], ['solver/bv/udiv8castdown7.btor.smt2'], ['solver/bv/udivtheorem1.btor.smt2'], ['solver/bv/ulttheorem1.btor.smt2'], ['solver/bv/umulo1.smt2'], ['solver/bv/umulo2.smt2'], ['solver/bv/uremtheorem1.btor.smt2'], ['solver/bv/uremudivaxiom4.btor.smt2'], ['solver/bv/uremudivaxiom4no.btor.smt2'], ['solver/bv/usubo1.smt2'], ['solver/bv/usubo2.smt2'], ['solver/bv/var1.btor.smt2'], ['solver/bv/var2.btor.smt2'], ['solver/fp/Float-no-simp1-main.smt2'], ['solver/fp/Float-no-simp3-main.smt2'], ['solver/fp/checkmodelfp1.smt2'], ['solver/fp/fp_fromsbv.smt2'], ['solver/fp/fp_fromsbv2.smt2'], ['solver/fp/fp_inf.smt2'], ['solver/fp/fp_max.smt2'], ['solver/fp/fp_min.smt2'], ['solver/fp/fp_misc.smt2'], ['solver/fp/fp_nan.smt2'], ['solver/fp/fp_rational.smt2'], ['solver/fp/fp_real.smt2'], ['solver/fp/fp_regr1.smt2'], ['solver/fp/fp_regr10.smt2'], ['solver/fp/fp_regr11.smt2'], ['solver/fp/fp_regr12.smt2'], ['solver/fp/fp_regr13.smt2'], ['solver/fp/fp_regr14.smt2'], ['solver/fp/fp_regr2.smt2'], ['solver/fp/fp_regr3.smt2'], ['solver/fp/fp_regr4.smt2'], ['solver/fp/fp_regr5.smt2', ['--bv-solver=prop']], ['solver/fp/fp_regr5.smt2'], ['solver/fp/fp_regr6.smt2'], ['solver/fp/fp_regr7.smt2'], ['solver/fp/fp_regr8.smt2'], ['solver/fp/fp_regr9.smt2'], ['solver/fp/fp_rm.smt2'], ['solver/fp/fp_sort.smt2'], ['solver/fp/fp_to_fp.smt2'], ['solver/fp/fp_zero.smt2'], ['solver/fp/uf_fpmax.smt2'], ['solver/fp/uf_fpmin.smt2'], ['solver/fp/uf_tosbv.smt2'], ['solver/fp/uf_toubv.smt2'], ['solver/fun/fun1.smt2'], ['solver/fun/nestedfun1.smt2', ['-rwl=2']], ['solver/fun/regrencparamapps.smt2'], ['solver/process_term1.smt2'], ['solver/process_term2.smt2'], ['solver/time_limit_per1.smt2'], ['solver/time_limit_per2.smt2'], ['solver/quant/duplicatelemma1.smt2'], ['solver/quant/issue96.smt2'], ['solver/quant/issue97.smt2'], ['solver/quant/quant_regr1.smt2'], ['solver/quant/quant_regr10.smt2'], ['solver/quant/quant_regr11.smt2'], ['solver/quant/quant_regr12.smt2'], ['solver/quant/quant_regr13.smt2'], ['solver/quant/quant_regr14.smt2'], ['solver/quant/quant_regr15.smt2'], ['solver/quant/quant_regr16.smt2'], ['solver/quant/quant_regr17.smt2'], ['solver/quant/quant_regr18.smt2'], ['solver/quant/quant_regr19.smt2'], ['solver/quant/quant_regr2.smt2'], ['solver/quant/quant_regr20.smt2'], ['solver/quant/quant_regr21.smt2'], ['solver/quant/quant_regr22.smt2'], ['solver/quant/quant_regr23.smt2'], ['solver/quant/quant_regr24.smt2'], ['solver/quant/quant_regr25.smt2'], #['solver/quant/quant_regr26.smt2'], # TODO: timeout ['solver/quant/quant_regr27.smt2'], ['solver/quant/quant_regr28.smt2'], ['solver/quant/quant_regr29.smt2'], ['solver/quant/quant_regr3.smt2'], ['solver/quant/quant_regr4.smt2'], ['solver/quant/quant_regr5.smt2'], ['solver/quant/quant_regr6.smt2'], ['solver/quant/quant_regr7.smt2'], ['solver/quant/quant_regr8.smt2'], ['solver/quant/quant_regr9.smt2'], ['solver/quant/regrnormquant.smt2'], ['solver/quant/regsmtparselet.smt2'], ] if get_option('b_sanitize') == 'none' # Regression test leads to false positives with ASAN due to gmp built with # assembly code by default (gmp can be built without via --disable-assembly, # see https://gmplib.org/manual/Build-Options). tests_smt2 += [['solver/bv/prop/prop_bvurem.smt2', ['--bv-solver=preprop']]] endif tests_btor2_parser = [ ['parser/btor2perr000.btor2'], ['parser/btor2perr001.btor2'], ['parser/btor2perr002.btor2'], ['parser/btor2perr003.btor2'], ['parser/btor2perr004.btor2'], ['parser/btor2perr005.btor2'], ['parser/btor2perr006.btor2'], ['parser/btor2perr007.btor2'], ['parser/btor2perr008.btor2'], ['parser/btor2perr009.btor2'], ['parser/btor2perr010.btor2'], ['parser/btor2perr011.btor2'], ['parser/btor2perr012.btor2'], ] tests_btor2_sat = [ #['preprocess/bv/normalize_add_incomplete.btor', ['-db']], #['preprocess/bv/normalize_and_incomplete.btor', ['-db']], #['preprocess/bv/normalize_mul_incomplete.btor', ['-db']], #['preprocess/bv/regaddnorm1.btor', ['-db']], #['preprocess/bv/regaddnorm2.btor', ['-db']], #['parser/arrayeqerr0.btor'], #['parser/arrayeqerr1.btor'], #['parser/arrayeqerr2.btor'], #['parser/btorperr000.btor'], #['parser/btorperr001.btor'], #['parser/btorperr002.btor'], #['parser/btorperr003.btor'], #['rewrite/array/rwr1.btor', ['-br all']], # TODO disabled because of -br #['solver/array/regrbetacache1.btor', ['-br all']], # TODO disabled because of -br #['solver/array/regrbetacache2.btor', ['-br all']], # currently broken since we don't allow to mix lambdas with arrays # TODO disabled because of -br #['solver/bv/concatslice1.btor', ['-rwl=1 -db']], #['solver/bv/concatslice2.btor', ['-rwl=1 -db']], #['solver/bv/regnegadd1.btor', ['-db']], #['solver/bv/regr-5smod3.btor', ['-m -d']], # TODO disabled because of -d #['solver/bv/regr-5srem3.btor', ['-m -d']], # TODO disabled because of -d #['solver/bv/regr-6smod3.btor', ['-m -d']], # TODO disabled because of -d #['solver/bv/regr-6srem3.btor', ['-m -d']], # TODO disabled because of -d #['solver/bv/regr5smod-3.btor', ['-m -d']], # TODO disabled because of -d #['solver/bv/regr5srem-3.btor', ['-m -d']], # TODO disabled because of -d #['solver/bv/regr6smod-3.btor', ['-m -d']], # TODO disabled because of -d #['solver/bv/regr6srem-3.btor', ['-m -d']], # TODO disabled because of -d ['preprocess/array/regrembeddedconstraint10.btor2'], ['preprocess/array/regrembeddedconstraint5.btor2'], ['preprocess/array/regrembeddedconstraint6.btor2'], ['preprocess/array/regrembeddedconstraint7.btor2'], ['preprocess/array/regrembeddedconstraint8.btor2'], ['preprocess/bv/normaddneg0.btor2'], ['preprocess/bv/normaddneg1.btor2'], ['preprocess/bv/regrembeddedconstraint11.btor2'], ['preprocess/bv/regrembeddedconstraint3.btor2'], ['preprocess/bv/regrembeddedconstraint9.btor2'], ['preprocess/bv/substcyclic1.btor2'], ['preprocess/bv/substitute1.btor2'], ['preprocess/bv/substitute3.btor2'], ['preprocess/bv/substitute4.btor2'], ['preprocess/bv/substitute40.btor2'], ['preprocess/bv/substitute5.btor2'], ['solver/array/random1.btor2'], ['preprocess/bv/ultsubst1.btor2'], ['preprocess/bv/ultsubst2.btor2'], ['preprocess/bv/ultsubst3.btor2'], ['preprocess/bv/ultsubst4.btor2'], ['preprocess/bv/ultsubst5.btor2'], ['preprocess/bv/ultsubst6.btor2'], ['preprocess/bv/ultsubst7.btor2'], ['preprocess/bv/ultsubst8.btor2'], ['preprocess/bv/ultsubst9.btor2'], ['rewrite/array/regr3vl1.btor2', ['-rwl=0']], ['rewrite/array/regr3vl1.btor2', ['-rwl=1']], ['rewrite/array/regr3vl1.btor2', ['-rwl=2']], ['rewrite/array/regr3vl2.btor2', ['-rwl=0']], ['rewrite/array/regr3vl2.btor2', ['-rwl=1']], ['rewrite/array/regr3vl2.btor2', ['-rwl=2']], ['rewrite/array/regr3vl3.btor2', ['-rwl=0']], ['rewrite/array/regr3vl3.btor2', ['-rwl=1']], ['rewrite/array/regr3vl3.btor2', ['-rwl=2']], ['rewrite/array/regr3vl4.btor2', ['-rwl=0']], ['rewrite/array/regr3vl4.btor2', ['-rwl=1']], ['rewrite/array/regr3vl4.btor2', ['-rwl=2']], ['rewrite/array/regrbfs1.btor2', ['-rwl=0']], ['rewrite/array/regrbfs1.btor2', ['-rwl=1']], ['rewrite/array/regrbfs1.btor2', ['-rwl=2']], ['rewrite/array/rw134.btor2'], ['rewrite/array/rw16.btor2'], ['rewrite/array/rw17.btor2'], ['rewrite/array/rw18.btor2'], ['rewrite/array/rwpropindexpluszero1.btor2'], ['rewrite/array/rwpropindexpluszero2.btor2'], ['rewrite/array/rwpropindexpluszero3.btor2'], ['rewrite/array/rwpropindexpluszero4.btor2'], ['rewrite/array/rwpropindexpluszero5.btor2'], ['rewrite/array/rwpropindexpluszero6.btor2'], ['rewrite/array/rwpropindexpluszero7.btor2'], ['rewrite/array/rwpropindexpluszero8.btor2'], ['rewrite/array/rww1.btor2'], ['rewrite/bv/rw1.btor2'], ['rewrite/bv/rw10.btor2'], ['rewrite/bv/rw11.btor2'], ['rewrite/bv/rw113.btor2'], ['rewrite/bv/rw114.btor2'], ['rewrite/bv/rw12.btor2'], ['rewrite/bv/rw121.btor2'], ['rewrite/bv/rw122.btor2'], ['rewrite/bv/rw13.btor2'], ['rewrite/bv/rw132.btor2'], ['rewrite/bv/rw133.btor2'], ['rewrite/bv/rw135.btor2'], ['rewrite/bv/rw137.btor2'], ['rewrite/bv/rw138.btor2'], ['rewrite/bv/rw139.btor2'], ['rewrite/bv/rw14.btor2'], ['rewrite/bv/rw140.btor2'], ['rewrite/bv/rw141.btor2'], ['rewrite/bv/rw142.btor2'], ['rewrite/bv/rw143.btor2'], ['rewrite/bv/rw148.btor2'], ['rewrite/bv/rw15.btor2'], ['rewrite/bv/rw153.btor2'], ['rewrite/bv/rw157.btor2'], ['rewrite/bv/rw166.btor2'], ['rewrite/bv/rw167.btor2'], ['rewrite/bv/rw168.btor2'], ['rewrite/bv/rw169.btor2'], ['rewrite/bv/rw179.btor2'], ['rewrite/bv/rw2.btor2'], ['rewrite/bv/rw3.btor2'], ['rewrite/bv/rw4.btor2'], ['rewrite/bv/rw44.btor2'], ['rewrite/bv/rw45.btor2'], ['rewrite/bv/rw5.btor2'], ['rewrite/bv/rw58.btor2'], ['rewrite/bv/rw59.btor2'], ['rewrite/bv/rw6.btor2'], ['rewrite/bv/rw7.btor2'], ['rewrite/bv/rw8.btor2'], ['rewrite/bv/rw9.btor2'], ['solver/array/arraycond1.btor2'], ['solver/array/arraycond10.btor2'], ['solver/array/arraycond15.btor2'], ['solver/array/arraycond16.btor2'], ['solver/array/arraycond17.btor2'], ['solver/array/arraycond2.btor2'], ['solver/array/arraycond4.btor2'], ['solver/array/ext1.btor2'], ['solver/array/ext12.btor2'], ['solver/array/ext14.btor2'], ['solver/array/ext17.btor2'], ['solver/array/ext20.btor2'], ['solver/array/ext3.btor2'], ['solver/array/ext4.btor2'], ['solver/array/ext6.btor2'], ['solver/array/ext8.btor2'], ['solver/array/invalidmodel3.btor2'], ['solver/array/lazyreadwritebug1.btor2'], ['solver/array/random1.btor2'], ['solver/array/random2.btor2'], ['solver/array/random3.btor2'], ['solver/array/random4.btor2'], ['solver/array/read12.btor2'], ['solver/array/read13.btor2'], ['solver/array/read14.btor2'], ['solver/array/read15.btor2'], ['solver/array/read18.btor2'], ['solver/array/read3.btor2'], ['solver/array/regprim11simp.btor2'], ['solver/array/regprim11simp.btor2'], ['solver/array/upprop1.btor2'], ['solver/array/write11.btor2'], ['solver/array/write12.btor2'], ['solver/array/write15.btor2'], ['solver/array/write18.btor2'], ['solver/array/write19.btor2'], ['solver/array/write20.btor2'], ['solver/array/write5.btor2'], ['solver/bv/const1.btor2'], ['solver/bv/factor18446744073709551617const.btor2'], ['solver/bv/factor18446744073709551617xconst.btor2'], ['solver/bv/factor18446744073709551617yconst.btor2'], ['solver/bv/factor2209.btor2'], ['solver/bv/factor4294967295.btor2'], ['solver/bv/factor4294967297.btor2'], ['solver/bv/lin0.btor2'], ['solver/bv/lin1.btor2'], ['solver/bv/lin2.btor2'], ['solver/bv/lin3.btor2'], ['solver/bv/lin4.btor2'], ['solver/bv/proxybug.btor2'], ['solver/bv/redand3twice.btor2'], ['solver/bv/redor3.btor2'], ['solver/bv/regrdomabst3.btor2'], ['solver/bv/regrdomabst4.btor2'], ['solver/bv/regrmark1.btor2'], ['solver/bv/regrrwbinexpconcatzeroconst.btor2'], ['solver/bv/regrw8simp.btor2'], ['solver/bv/rol_same_bw.btor2'], ['solver/bv/ror_same_bw.btor2'], ['solver/bv/slicesubst1.btor2'], ['solver/bv/sll_same_bw.btor2'], ['solver/bv/sqrt25.btor2'], ['solver/bv/sqrt4.btor2'], ['solver/bv/sqrt4295098369.btor2'], ['solver/bv/sqrt49.btor2'], ['solver/bv/sqrt9.btor2'], ['solver/bv/srl_same_bw.btor2'], ['solver/bv/var1.btor2'], ['solver/bv/var2.btor2'], ] tests_btor2_unsat = [ #['rewrite/bv/rw48.btor2'], # TODO too slow #['rewrite/bv/rw49.btor2'], # TODO too slow #['rewrite/bv/rw50.btor2'], # TODO too slow (timeout after 150s) #['rewrite/bv/rw60.btor2'], # TODO too slow (timeout after 150s) ['preprocess/array/regrembeddedconstraint1.btor2'], ['preprocess/array/regrembeddedconstraint12.btor2', ['-rwl=0']], ['preprocess/array/regrembeddedconstraint12.btor2', ['-rwl=1']], ['preprocess/array/regrembeddedconstraint12.btor2', ['-rwl=2']], ['preprocess/array/regrembeddedconstraint13.btor2', ['-rwl=0']], ['preprocess/array/regrembeddedconstraint13.btor2', ['-rwl=1']], ['preprocess/array/regrembeddedconstraint13.btor2', ['-rwl=2']], ['preprocess/array/regrembeddedconstraint2.btor2', ['-rwl=0']], ['preprocess/array/regrembeddedconstraint2.btor2', ['-rwl=1']], ['preprocess/array/regrembeddedconstraint2.btor2', ['-rwl=2']], ['preprocess/array/regrembeddedconstraint4.btor2', ['-rwl=0']], ['preprocess/array/regrembeddedconstraint4.btor2', ['-rwl=1']], ['preprocess/array/regrembeddedconstraint4.btor2', ['-rwl=2']], ['preprocess/bv/normaddneg2.btor2'], ['preprocess/bv/normaddneg3.btor2'], ['preprocess/bv/regrembeddedconstraint14.btor2'], ['preprocess/bv/substitute10.btor2'], ['preprocess/bv/substitute11.btor2'], ['preprocess/bv/substitute12.btor2'], ['preprocess/bv/substitute13.btor2'], ['preprocess/bv/substitute14.btor2'], ['preprocess/bv/substitute15.btor2'], ['preprocess/bv/substitute16.btor2'], ['preprocess/bv/substitute17.btor2'], ['preprocess/bv/substitute18.btor2'], ['preprocess/bv/substitute19.btor2'], ['preprocess/bv/substitute2.btor2'], ['preprocess/bv/substitute20.btor2'], ['preprocess/bv/substitute21.btor2'], ['preprocess/bv/substitute22.btor2'], ['preprocess/bv/substitute23.btor2'], ['preprocess/bv/substitute24.btor2'], ['preprocess/bv/substitute25.btor2'], ['preprocess/bv/substitute26.btor2'], ['preprocess/bv/substitute27.btor2'], ['preprocess/bv/substitute28.btor2'], ['preprocess/bv/substitute29.btor2'], ['preprocess/bv/substitute30.btor2'], ['preprocess/bv/substitute31.btor2'], ['preprocess/bv/substitute32.btor2'], ['preprocess/bv/substitute33.btor2'], ['preprocess/bv/substitute34.btor2'], ['preprocess/bv/substitute35.btor2'], ['preprocess/bv/substitute36.btor2'], ['preprocess/bv/substitute37.btor2'], ['preprocess/bv/substitute38.btor2'], ['preprocess/bv/substitute39.btor2'], ['preprocess/bv/substitute6.btor2'], ['preprocess/bv/substitute7.btor2'], ['preprocess/bv/substitute8.btor2'], ['preprocess/bv/substitute9.btor2'], ['rewrite/array/rw115.btor2'], ['rewrite/array/rw116.btor2'], ['rewrite/array/rw123.btor2'], ['rewrite/array/rw124.btor2'], ['rewrite/array/rw30.btor2'], ['rewrite/array/rw31.btor2'], ['rewrite/array/rw32.btor2'], ['rewrite/array/rw33.btor2'], ['rewrite/array/rw34.btor2'], ['rewrite/array/rw35.btor2'], ['rewrite/array/rw92.btor2'], ['rewrite/array/rw93.btor2'], ['rewrite/array/rwpropindexplusconst1.btor2'], ['rewrite/array/rwpropindexplusconst2.btor2'], ['rewrite/array/rwpropindexplusconst3.btor2'], ['rewrite/array/rwpropindexplusconst4.btor2'], ['rewrite/bv/3vl2.btor2'], ['rewrite/bv/3vl3.btor2'], ['rewrite/bv/3vl4.btor2'], ['rewrite/bv/3vl5.btor2'], ['rewrite/bv/3vl6.btor2'], ['rewrite/bv/rw100.btor2'], ['rewrite/bv/rw101.btor2'], ['rewrite/bv/rw102.btor2'], ['rewrite/bv/rw103.btor2'], ['rewrite/bv/rw104.btor2'], ['rewrite/bv/rw105.btor2'], ['rewrite/bv/rw106.btor2'], ['rewrite/bv/rw107.btor2'], ['rewrite/bv/rw108.btor2'], ['rewrite/bv/rw109.btor2'], ['rewrite/bv/rw110.btor2'], ['rewrite/bv/rw111.btor2'], ['rewrite/bv/rw112.btor2'], ['rewrite/bv/rw117.btor2'], ['rewrite/bv/rw118.btor2'], ['rewrite/bv/rw119.btor2'], ['rewrite/bv/rw120.btor2'], ['rewrite/bv/rw125.btor2'], ['rewrite/bv/rw126.btor2'], ['rewrite/bv/rw127.btor2'], ['rewrite/bv/rw128.btor2'], ['rewrite/bv/rw129.btor2'], ['rewrite/bv/rw130.btor2'], ['rewrite/bv/rw131.btor2'], ['rewrite/bv/rw136.btor2'], ['rewrite/bv/rw144.btor2'], ['rewrite/bv/rw145.btor2'], ['rewrite/bv/rw146.btor2'], ['rewrite/bv/rw147.btor2'], ['rewrite/bv/rw149.btor2'], ['rewrite/bv/rw150.btor2'], ['rewrite/bv/rw151.btor2'], ['rewrite/bv/rw152.btor2'], ['rewrite/bv/rw154.btor2'], ['rewrite/bv/rw155.btor2'], ['rewrite/bv/rw156.btor2'], ['rewrite/bv/rw158.btor2', ['-rwl=1']], ['rewrite/bv/rw159.btor2', ['-rwl=1']], ['rewrite/bv/rw160.btor2', ['-rwl=1']], ['rewrite/bv/rw161.btor2', ['-rwl=1']], ['rewrite/bv/rw162.btor2', ['-rwl=1']], ['rewrite/bv/rw163.btor2', ['-rwl=1']], ['rewrite/bv/rw164.btor2', ['-rwl=1']], ['rewrite/bv/rw165.btor2', ['-rwl=1']], ['rewrite/bv/rw170.btor2', ['-rwl=1']], ['rewrite/bv/rw171.btor2', ['-rwl=1']], ['rewrite/bv/rw172.btor2', ['-rwl=1']], ['rewrite/bv/rw173.btor2', ['-rwl=1']], ['rewrite/bv/rw174.btor2', ['-rwl=1']], ['rewrite/bv/rw175.btor2', ['-rwl=1']], ['rewrite/bv/rw176.btor2', ['-rwl=1']], ['rewrite/bv/rw177.btor2', ['-rwl=1']], ['rewrite/bv/rw180.btor2'], ['rewrite/bv/rw181.btor2'], ['rewrite/bv/rw182.btor2'], ['rewrite/bv/rw183.btor2'], ['rewrite/bv/rw184.btor2'], ['rewrite/bv/rw185.btor2'], ['rewrite/bv/rw186.btor2'], ['rewrite/bv/rw187.btor2'], ['rewrite/bv/rw188.btor2'], ['rewrite/bv/rw189.btor2'], ['rewrite/bv/rw19.btor2'], ['rewrite/bv/rw190.btor2'], ['rewrite/bv/rw191.btor2'], ['rewrite/bv/rw192.btor2'], ['rewrite/bv/rw193.btor2'], ['rewrite/bv/rw194.btor2'], ['rewrite/bv/rw195.btor2'], ['rewrite/bv/rw196.btor2'], ['rewrite/bv/rw197.btor2'], ['rewrite/bv/rw198.btor2'], ['rewrite/bv/rw199.btor2'], ['rewrite/bv/rw20.btor2'], ['rewrite/bv/rw200.btor2'], ['rewrite/bv/rw201.btor2'], ['rewrite/bv/rw202.btor2'], ['rewrite/bv/rw203.btor2'], ['rewrite/bv/rw204.btor2'], ['rewrite/bv/rw205.btor2'], ['rewrite/bv/rw206.btor2'], ['rewrite/bv/rw207.btor2'], ['rewrite/bv/rw208.btor2'], ['rewrite/bv/rw209.btor2'], ['rewrite/bv/rw21.btor2'], ['rewrite/bv/rw210.btor2'], ['rewrite/bv/rw211.btor2'], ['rewrite/bv/rw22.btor2'], ['rewrite/bv/rw23.btor2'], ['rewrite/bv/rw24.btor2'], ['rewrite/bv/rw25.btor2'], ['rewrite/bv/rw26.btor2'], ['rewrite/bv/rw27.btor2'], ['rewrite/bv/rw28.btor2'], ['rewrite/bv/rw29.btor2'], ['rewrite/bv/rw36.btor2'], ['rewrite/bv/rw37.btor2'], ['rewrite/bv/rw38.btor2'], ['rewrite/bv/rw39.btor2'], ['rewrite/bv/rw40.btor2'], ['rewrite/bv/rw41.btor2'], ['rewrite/bv/rw42.btor2'], ['rewrite/bv/rw43.btor2'], ['rewrite/bv/rw46.btor2'], ['rewrite/bv/rw47.btor2'], ['rewrite/bv/rw51.btor2'], ['rewrite/bv/rw52.btor2'], ['rewrite/bv/rw53.btor2'], ['rewrite/bv/rw54.btor2'], ['rewrite/bv/rw55.btor2'], ['rewrite/bv/rw56.btor2'], ['rewrite/bv/rw57.btor2'], ['rewrite/bv/rw61.btor2'], ['rewrite/bv/rw62.btor2'], ['rewrite/bv/rw63.btor2'], ['rewrite/bv/rw64.btor2'], ['rewrite/bv/rw65.btor2'], ['rewrite/bv/rw66.btor2'], ['rewrite/bv/rw67.btor2'], ['rewrite/bv/rw68.btor2'], ['rewrite/bv/rw69.btor2'], ['rewrite/bv/rw70.btor2'], ['rewrite/bv/rw71.btor2'], ['rewrite/bv/rw72.btor2'], ['rewrite/bv/rw73.btor2'], ['rewrite/bv/rw74.btor2'], ['rewrite/bv/rw75.btor2'], ['rewrite/bv/rw76.btor2'], ['rewrite/bv/rw77.btor2'], ['rewrite/bv/rw78.btor2'], ['rewrite/bv/rw79.btor2'], ['rewrite/bv/rw80.btor2'], ['rewrite/bv/rw81.btor2'], ['rewrite/bv/rw82.btor2'], ['rewrite/bv/rw83.btor2'], ['rewrite/bv/rw84.btor2'], ['rewrite/bv/rw85.btor2'], ['rewrite/bv/rw86.btor2'], ['rewrite/bv/rw87.btor2'], ['rewrite/bv/rw88.btor2'], ['rewrite/bv/rw89.btor2'], ['rewrite/bv/rw90.btor2'], ['rewrite/bv/rw91.btor2'], ['rewrite/bv/rw94.btor2'], ['rewrite/bv/rw95.btor2'], ['rewrite/bv/rw96.btor2'], ['rewrite/bv/rw97.btor2'], ['rewrite/bv/rw98.btor2'], ['rewrite/bv/rw99.btor2'], ['solver/array/3vl1.btor2', ['-rwl=0']], ['solver/array/3vl1.btor2', ['-rwl=2']], ['solver/array/arraycond11.btor2'], ['solver/array/arraycond12.btor2'], ['solver/array/arraycond13.btor2'], ['solver/array/arraycond14.btor2'], ['solver/array/arraycond18.btor2'], ['solver/array/arraycond3.btor2'], ['solver/array/arraycond5.btor2'], ['solver/array/arraycond6.btor2'], ['solver/array/arraycond7.btor2'], ['solver/array/arraycond8.btor2'], ['solver/array/arraycond9.btor2'], ['solver/array/arraycondconst.btor2', ['-rwl=0']], ['solver/array/arraycondconstaig.btor2', ['-rwl=0']], ['solver/array/ext10.btor2'], ['solver/array/ext11.btor2'], ['solver/array/ext13.btor2'], ['solver/array/ext15.btor2'], ['solver/array/ext16.btor2'], ['solver/array/ext18.btor2'], ['solver/array/ext19.btor2'], ['solver/array/ext2.btor2'], ['solver/array/ext21.btor2'], ['solver/array/ext22.btor2'], ['solver/array/ext23.btor2'], ['solver/array/ext24.btor2'], ['solver/array/ext25.btor2'], ['solver/array/ext26.btor2'], ['solver/array/ext27.btor2'], ['solver/array/ext28.btor2'], ['solver/array/ext29.btor2'], ['solver/array/ext5.btor2'], ['solver/array/ext7.btor2'], ['solver/array/ext9.btor2'], ['solver/array/extarraywrite1.btor2'], ['solver/array/extarraywrite2.btor2'], ['solver/array/random5.btor2', ['-rwl=0']], ['solver/array/random5.btor2', ['-rwl=1']], ['solver/array/read1.btor2'], ['solver/array/read10.btor2'], ['solver/array/read11.btor2'], ['solver/array/read16.btor2'], ['solver/array/read17.btor2'], ['solver/array/read19.btor2'], ['solver/array/read2.btor2'], ['solver/array/read20.btor2'], ['solver/array/read21.btor2'], ['solver/array/read22.btor2'], ['solver/array/read4.btor2'], ['solver/array/read5.btor2'], ['solver/array/read6.btor2'], ['solver/array/read7.btor2'], ['solver/array/read8.btor2'], ['solver/array/read9.btor2'], ['solver/array/regrexpleak2.btor2', ['-rwl=1']], ['solver/array/regrmark2.btor2', ['-rwl=0']], ['solver/array/regrmark2.btor2', ['-rwl=1']], ['solver/array/regrmark2.btor2', ['-rwl=2']], ['solver/array/regrmark3.btor2', ['-rwl=0']], ['solver/array/regrmark3.btor2', ['-rwl=1']], ['solver/array/regrmark3.btor2', ['-rwl=2']], ['solver/array/write1.btor2'], ['solver/array/write10.btor2'], ['solver/array/write13.btor2'], ['solver/array/write14.btor2'], ['solver/array/write16.btor2'], ['solver/array/write17.btor2'], ['solver/array/write2.btor2'], ['solver/array/write21.btor2'], ['solver/array/write22.btor2'], ['solver/array/write23.btor2'], ['solver/array/write24.btor2'], ['solver/array/write3.btor2'], ['solver/array/write4.btor2'], ['solver/array/write6.btor2'], ['solver/array/write7.btor2'], ['solver/array/write8.btor2'], ['solver/array/write9.btor2'], ['solver/bv/addnegmul1.btor2'], ['solver/bv/andopt1.btor2'], ['solver/bv/andopt10.btor2'], ['solver/bv/andopt11.btor2'], ['solver/bv/andopt12.btor2'], ['solver/bv/andopt13.btor2'], ['solver/bv/andopt14.btor2'], ['solver/bv/andopt15.btor2'], ['solver/bv/andopt16.btor2'], ['solver/bv/andopt17.btor2'], ['solver/bv/andopt2.btor2'], ['solver/bv/andopt3.btor2'], ['solver/bv/andopt4.btor2'], ['solver/bv/andopt5.btor2'], ['solver/bv/andopt6.btor2'], ['solver/bv/andopt7.btor2'], ['solver/bv/andopt8.btor2'], ['solver/bv/andopt9.btor2'], ['solver/bv/const2.btor2'], ['solver/bv/dec_rwl0.btor2', ['-rwl=0']], ['solver/bv/dec_rwl3.btor2'], ['solver/bv/distri1.btor2'], ['solver/bv/distri2.btor2'], ['solver/bv/distri3.btor2'], ['solver/bv/distri4.btor2'], ['solver/bv/distri5.btor2'], ['solver/bv/distri6.btor2'], ['solver/bv/distri7.btor2'], ['solver/bv/distri8.btor2'], ['solver/bv/exactlyone.btor2'], ['solver/bv/gtewithsub.btor2'], ['solver/bv/hd1.btor2'], ['solver/bv/hd10.btor2'], ['solver/bv/hd11.btor2'], ['solver/bv/hd12.btor2'], ['solver/bv/hd13.btor2'], ['solver/bv/hd14.btor2'], ['solver/bv/hd15.btor2'], ['solver/bv/hd16.btor2'], ['solver/bv/hd17.btor2'], ['solver/bv/hd18.btor2'], ['solver/bv/hd19.btor2'], ['solver/bv/hd2.btor2'], ['solver/bv/hd20.btor2'], ['solver/bv/hd21.btor2'], ['solver/bv/hd3.btor2'], ['solver/bv/hd4.btor2'], ['solver/bv/hd5.btor2'], ['solver/bv/hd6.btor2'], ['solver/bv/hd7.btor2'], ['solver/bv/hd8.btor2'], ['solver/bv/hd9.btor2'], ['solver/bv/inc.btor2'], ['solver/bv/inc.btor2'], ['solver/bv/prim8bugreduced.btor2'], ['solver/bv/regrexpleak1.btor2'], ['solver/bv/regrpointerchasing1.btor2'], ['solver/bv/regsubslapd149921red.btor2'], ['solver/bv/sqrt13.btor2'], ['solver/bv/sqrt18446744073709551617.btor2'], ['solver/bv/sqrt29.btor2'], ['solver/bv/sqrt31.btor2'], ['solver/bv/sqrt4294967297.btor2'], ['solver/bv/sqrt5.btor2'], ['solver/bv/sqrt65537.btor2'], ['solver/bv/sqrt7.btor2'], ['solver/bv/sult.btor2'], ['solver/bv/sult2.btor2'], ['solver/bv/twocomplementassub.btor2'], ['solver/bv/udiv16castdown8.btor2'], ['solver/bv/udiv8castdown4.btor2'], ['solver/bv/udiv8castdown5.btor2'], ['solver/bv/udiv8castdown6.btor2'], ['solver/bv/udiv8castdown7.btor2'], ['solver/bv/udivtheorem1.btor2'], ['solver/bv/ulttheorem1.btor2'], ['solver/bv/uremtheorem1.btor2'], ['solver/bv/uremudivaxiom4.btor2'], ['solver/bv/uremudivaxiom4no.btor2'], ] regress_tests = [ [tests_smt2], [tests_smt2, [], ['--produce-unsat-cores', '--check-unsat-core']], [tests_btor2_parser], [tests_btor2_sat, '--check-sat'], [tests_btor2_unsat, '--check-unsat'], [tests_btor2_unsat, '--check-unsat', ['--produce-unsat-cores', '--check-unsat-core']], ] # Disable wine debug output if we run the cross-compiled binary env = [] if meson.is_cross_build() and host_machine.system() == 'windows' env += ['WINEDEBUG=fixme-all'] endif foreach t : regress_tests tests = t[0] run_regress_script_options = [] global_args = [] if t.length() >= 2 run_regress_script_options += t[1] endif if t.length() == 3 global_args += t[2] endif foreach test_args : tests file = test_args[0] name = file.replace('/', '_') test_case = [join_paths(meson.current_source_dir(), file)] test_case += global_args if test_args.length() == 2 test_case += test_args[1] endif args = [run_regress_script.full_path()] args += bitwuzla_bin.full_path() args += ' '.join(test_case) args += meson.current_build_dir() args += run_regress_script_options test(name, python, args: args, suite: 'regress', depends: bitwuzla_bin, timeout: 120, env: env) endforeach endforeach