summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bv
ModeNameSize
-rw-r--r--ackermann1.smt2409logplain
-rw-r--r--ackermann2.smt2535logplain
-rw-r--r--ackermann3.smt2517logplain
-rw-r--r--ackermann4.smt2395logplain
-rw-r--r--ackermann5.smt2574logplain
-rw-r--r--ackermann6.smt2582logplain
-rw-r--r--ackermann7.smt2408logplain
-rw-r--r--ackermann8.smt2434logplain
-rw-r--r--bool-model.smt2216logplain
-rw-r--r--bool-to-bv-all-array-bool.smt2541logplain
-rw-r--r--bool-to-bv-all-test.smt2662logplain
-rw-r--r--bool-to-bv-all.smt2536logplain
-rw-r--r--bool-to-bv-ite-array-bool.smt2541logplain
-rw-r--r--bool-to-bv-ite.smt2474logplain
-rw-r--r--bug260a.smtv1.smt2194logplain
-rw-r--r--bug260b.smtv1.smt2184logplain
-rw-r--r--bug345.smtv1.smt2815logplain
-rw-r--r--bug440.smtv1.smt23390logplain
-rw-r--r--bug733.smt2230logplain
-rw-r--r--bug734.smt2247logplain
-rw-r--r--bv-abstr-bug.smt2278logplain
-rw-r--r--bv-abstr-bug2.smt2207logplain
-rw-r--r--bv-int-collapse1.smt2188logplain
-rw-r--r--bv-int-collapse2.smt2178logplain
-rw-r--r--bv-options4.smt2498logplain
-rw-r--r--bv-to-bool1.smtv1.smt2135378logplain
-rw-r--r--bv-to-bool2.smt2179logplain
-rw-r--r--bv2nat-ground-c.smt2393logplain
-rw-r--r--bv2nat-simp-range.smt2200logplain
-rw-r--r--bv_to_int1.smt2308logplain
-rw-r--r--bv_to_int_5230_binary.smt2591logplain
-rw-r--r--bv_to_int_5230_missing_op.smt2172logplain
-rw-r--r--bv_to_int_5230_shift_const.smt2567logplain
-rw-r--r--bv_to_int_5281.smt2299logplain
-rw-r--r--bv_to_int_5293_1.smt2256logplain
-rw-r--r--bv_to_int_5293_2.smt2675logplain
-rw-r--r--bv_to_int_bvmul2.smt2289logplain
-rw-r--r--bv_to_int_bvuf_to_intuf.smt2261logplain
-rw-r--r--bv_to_int_bvuf_to_intuf_sorts.smt2427logplain
-rw-r--r--bv_to_int_elim_err.smt2325logplain
-rw-r--r--bv_to_int_zext.smt2274logplain
-rw-r--r--bvcomp.cvc55logplain
-rw-r--r--bvmul-pow2-only.smt2199logplain
-rw-r--r--bvsimple.cvc1165logplain
-rw-r--r--bvsmod.smt2831logplain
-rw-r--r--calc2_sec2_shifter_mult_bmc15.atlas.delta01.smtv1.smt21714logplain
d---------core4021logplain
-rw-r--r--div_mod.cvc250logplain
-rw-r--r--divtest_2_5.smt2188logplain
-rw-r--r--divtest_2_6.smt2220logplain
-rw-r--r--eager-force-logic.smt2246logplain
-rw-r--r--eager-inc-cadical.smt2472logplain
-rw-r--r--eager-inc-cryptominisat.smt2468logplain
-rw-r--r--fuzz01.smtv1.smt2135335logplain
-rw-r--r--fuzz02.delta01.smtv1.smt2245logplain
-rw-r--r--fuzz02.smtv1.smt25083logplain
-rw-r--r--fuzz03.smtv1.smt22573logplain
-rw-r--r--fuzz04.smtv1.smt27393logplain
-rw-r--r--fuzz05.smtv1.smt253611logplain
-rw-r--r--fuzz06.smtv1.smt28077logplain
-rw-r--r--fuzz07-delta.smtv1.smt2567logplain
-rw-r--r--fuzz07.smtv1.smt216135logplain
-rw-r--r--fuzz08.smtv1.smt2309logplain
-rw-r--r--fuzz09.smtv1.smt213414logplain
-rw-r--r--fuzz10.smtv1.smt2147logplain
-rw-r--r--fuzz11.smtv1.smt2230logplain
-rw-r--r--fuzz12.smtv1.smt2931logplain
-rw-r--r--fuzz13.smtv1.smt2403logplain
-rw-r--r--fuzz14.smtv1.smt2708logplain
-rw-r--r--fuzz15.delta01.smtv1.smt22123logplain
-rw-r--r--fuzz16.delta01.smtv1.smt21226logplain
-rw-r--r--fuzz17.delta01.smtv1.smt21963logplain
-rw-r--r--fuzz18.delta01.smtv1.smt22429logplain
-rw-r--r--fuzz18.delta02.smtv1.smt22238logplain
-rw-r--r--fuzz18.delta03.smtv1.smt2634logplain
-rw-r--r--fuzz19.delta01.smtv1.smt22744logplain
-rw-r--r--fuzz20.delta01.smtv1.smt2287logplain
-rw-r--r--fuzz20.smtv1.smt27856logplain
-rw-r--r--fuzz21.delta01.smtv1.smt2205logplain
-rw-r--r--fuzz21.smtv1.smt225265logplain
-rw-r--r--fuzz22.delta01.smtv1.smt21100logplain
-rw-r--r--fuzz22.smtv1.smt25411logplain
-rw-r--r--fuzz23.delta01.smtv1.smt2192logplain
-rw-r--r--fuzz23.smtv1.smt29755logplain
-rw-r--r--fuzz24.delta01.smtv1.smt2231logplain
-rw-r--r--fuzz24.smtv1.smt211527logplain
-rw-r--r--fuzz25.delta01.smtv1.smt2295logplain
-rw-r--r--fuzz25.smtv1.smt216626logplain
-rw-r--r--fuzz26.delta01.smtv1.smt2363logplain
-rw-r--r--fuzz26.smtv1.smt246366logplain
-rw-r--r--fuzz27.delta01.smtv1.smt2236logplain
-rw-r--r--fuzz27.smtv1.smt25404logplain
-rw-r--r--fuzz28.delta01.smtv1.smt2192logplain
-rw-r--r--fuzz28.smtv1.smt218066logplain
-rw-r--r--fuzz29.delta01.smtv1.smt21043logplain
-rw-r--r--fuzz29.smtv1.smt23365logplain
-rw-r--r--fuzz30.delta01.smtv1.smt2228logplain
-rw-r--r--fuzz30.smtv1.smt22355logplain
-rw-r--r--fuzz31.delta01.smtv1.smt2264logplain
-rw-r--r--fuzz31.smtv1.smt220862logplain
-rw-r--r--fuzz32.delta01.smtv1.smt2402logplain
-rw-r--r--fuzz32.smtv1.smt263856logplain
-rw-r--r--fuzz33.delta01.smtv1.smt2192logplain
-rw-r--r--fuzz33.smtv1.smt25501logplain
-rw-r--r--fuzz34.delta01.smtv1.smt2377logplain
-rw-r--r--fuzz35.delta01.smtv1.smt2230logplain
-rw-r--r--fuzz35.smtv1.smt213828logplain
-rw-r--r--fuzz36.delta01.smtv1.smt2822logplain
-rw-r--r--fuzz36.smtv1.smt214276logplain
-rw-r--r--fuzz37.delta01.smtv1.smt2262logplain
-rw-r--r--fuzz37.smtv1.smt24691logplain
-rw-r--r--fuzz38.delta01.smtv1.smt2314logplain
-rw-r--r--fuzz39.delta01.smtv1.smt2264logplain
-rw-r--r--fuzz39.smtv1.smt24332logplain
-rw-r--r--fuzz40.delta01.smtv1.smt2188logplain
-rw-r--r--fuzz40.smtv1.smt24591logplain
-rw-r--r--fuzz41.smtv1.smt28967logplain
-rw-r--r--incorrect1.delta01.smtv1.smt2166logplain
-rw-r--r--inequality00.smt2459logplain
-rw-r--r--inequality01.smt2489logplain
-rw-r--r--inequality02.smt2491logplain
-rw-r--r--inequality03.smt2222logplain
-rw-r--r--inequality04.smt2443logplain
-rw-r--r--inequality05.smt2643logplain
-rw-r--r--int_to_bv_err_on_demand_1.smt2279logplain
-rw-r--r--int_to_bv_model.smt2208logplain
-rw-r--r--int_to_bv_model2.smt2144logplain
-rw-r--r--issue-4075.smt2316logplain
-rw-r--r--issue-4076.smt2348logplain
-rw-r--r--issue-4130.smt2346logplain
-rw-r--r--issue3621.smt2114logplain
-rw-r--r--issue5396.smt2286logplain
-rw-r--r--mul-neg-unsat.smt2179logplain
-rw-r--r--mul-negpow2.smt2198logplain
-rw-r--r--mult-pow2-negative.smt2151logplain
-rw-r--r--pr4993-bvugt-bvurem-a.smt2211logplain
-rw-r--r--pr4993-bvugt-bvurem-b.smt2257logplain
-rw-r--r--reset-assertions-assert-input.smt2413logplain
-rw-r--r--sizecheck.cvc113logplain
-rw-r--r--smtcompbug.smtv1.smt2418logplain
-rw-r--r--temp.lrat0logplain
-rw-r--r--test-bv_intro_pow2.smt2598logplain
-rw-r--r--test00.smtv1.smt21083logplain
-rw-r--r--unsound1-reduced.smt2319logplain
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback