git.libre-soc.org Git - cvc5.git/tree - test/regress/cli/regress0/bv/

drwxr-xr-x		..
-rw-r--r--	397	ackermann1.smt2	blob \| history \| raw
-rw-r--r--	535	ackermann2.smt2	blob \| history \| raw
-rw-r--r--	489	ackermann3.smt2	blob \| history \| raw
-rw-r--r--	401	ackermann4.smt2	blob \| history \| raw
-rw-r--r--	574	ackermann5.smt2	blob \| history \| raw
-rw-r--r--	582	ackermann6.smt2	blob \| history \| raw
-rw-r--r--	408	ackermann7.smt2	blob \| history \| raw
-rw-r--r--	434	ackermann8.smt2	blob \| history \| raw
-rw-r--r--	216	bool-model.smt2	blob \| history \| raw
-rw-r--r--	541	bool-to-bv-all-array-bool.smt2	blob \| history \| raw
-rw-r--r--	662	bool-to-bv-all-test.smt2	blob \| history \| raw
-rw-r--r--	536	bool-to-bv-all.smt2	blob \| history \| raw
-rw-r--r--	541	bool-to-bv-ite-array-bool.smt2	blob \| history \| raw
-rw-r--r--	474	bool-to-bv-ite.smt2	blob \| history \| raw
-rw-r--r--	194	bug260a.smtv1.smt2	blob \| history \| raw
-rw-r--r--	184	bug260b.smtv1.smt2	blob \| history \| raw
-rw-r--r--	815	bug345.smtv1.smt2	blob \| history \| raw
-rw-r--r--	3390	bug440.smtv1.smt2	blob \| history \| raw
-rw-r--r--	230	bug733.smt2	blob \| history \| raw
-rw-r--r--	247	bug734.smt2	blob \| history \| raw
-rw-r--r--	207	bv-abstr-bug2.smt2	blob \| history \| raw
-rw-r--r--	188	bv-int-collapse1.smt2	blob \| history \| raw
-rw-r--r--	178	bv-int-collapse2.smt2	blob \| history \| raw
-rw-r--r--	498	bv-options4.smt2	blob \| history \| raw
-rw-r--r--	135378	bv-to-bool1.smtv1.smt2	blob \| history \| raw
-rw-r--r--	179	bv-to-bool2.smt2	blob \| history \| raw
-rw-r--r--	393	bv2nat-ground-c.smt2	blob \| history \| raw
-rw-r--r--	200	bv2nat-simp-range.smt2	blob \| history \| raw
-rw-r--r--	380	bv_to_int1.smt2	blob \| history \| raw
-rw-r--r--	280	bv_to_int_415.smt2	blob \| history \| raw
-rw-r--r--	591	bv_to_int_5230_binary.smt2	blob \| history \| raw
-rw-r--r--	172	bv_to_int_5230_missing_op.smt2	blob \| history \| raw
-rw-r--r--	567	bv_to_int_5230_shift_const.smt2	blob \| history \| raw
-rw-r--r--	284	bv_to_int_5281.smt2	blob \| history \| raw
-rw-r--r--	256	bv_to_int_5293_1.smt2	blob \| history \| raw
-rw-r--r--	675	bv_to_int_5293_2.smt2	blob \| history \| raw
-rw-r--r--	183	bv_to_int_8412.smt2	blob \| history \| raw
-rw-r--r--	338	bv_to_int_bvmul2.smt2	blob \| history \| raw
-rw-r--r--	333	bv_to_int_bvuf_to_intuf.smt2	blob \| history \| raw
-rw-r--r--	499	bv_to_int_bvuf_to_intuf_sorts.smt2	blob \| history \| raw
-rw-r--r--	395	bv_to_int_elim_err.smt2	blob \| history \| raw
-rw-r--r--	290	bv_to_int_int1.smt2	blob \| history \| raw
-rw-r--r--	212	bv_to_int_issue_8413_1.smt2	blob \| history \| raw
-rw-r--r--	220	bv_to_int_issue_8413_2.smt2	blob \| history \| raw
-rw-r--r--	182	bv_to_int_proj_417.smt2	blob \| history \| raw
-rw-r--r--	346	bv_to_int_zext.smt2	blob \| history \| raw
-rw-r--r--	138	bvcomp.cvc.smt2	blob \| history \| raw
-rw-r--r--	199	bvmul-pow2-only.smt2	blob \| history \| raw
-rw-r--r--	160	bvproof1.smt2	blob \| history \| raw
-rw-r--r--	429	bvproof2.smt2	blob \| history \| raw
-rw-r--r--	164	bvproof3.smt2	blob \| history \| raw
-rw-r--r--	1606	bvsimple.cvc.smt2	blob \| history \| raw
-rw-r--r--	831	bvsmod.smt2	blob \| history \| raw
-rw-r--r--	1714	calc2_sec2_shifter_mult_bmc15.atlas.delta01.smtv1.smt2	blob \| history \| raw
drwxr-xr-x	-	core	tree \| history
-rw-r--r--	351	div_mod.cvc.smt2	blob \| history \| raw
-rw-r--r--	188	divtest_2_5.smt2	blob \| history \| raw
-rw-r--r--	220	divtest_2_6.smt2	blob \| history \| raw
-rw-r--r--	246	eager-force-logic.smt2	blob \| history \| raw
-rw-r--r--	472	eager-inc-cadical.smt2	blob \| history \| raw
-rw-r--r--	468	eager-inc-cryptominisat.smt2	blob \| history \| raw
-rw-r--r--	135335	fuzz01.smtv1.smt2	blob \| history \| raw
-rw-r--r--	245	fuzz02.delta01.smtv1.smt2	blob \| history \| raw
-rw-r--r--	5083	fuzz02.smtv1.smt2	blob \| history \| raw
-rw-r--r--	2573	fuzz03.smtv1.smt2	blob \| history \| raw
-rw-r--r--	7393	fuzz04.smtv1.smt2	blob \| history \| raw
-rw-r--r--	53611	fuzz05.smtv1.smt2	blob \| history \| raw
-rw-r--r--	8077	fuzz06.smtv1.smt2	blob \| history \| raw
-rw-r--r--	567	fuzz07-delta.smtv1.smt2	blob \| history \| raw
-rw-r--r--	16135	fuzz07.smtv1.smt2	blob \| history \| raw
-rw-r--r--	309	fuzz08.smtv1.smt2	blob \| history \| raw
-rw-r--r--	13414	fuzz09.smtv1.smt2	blob \| history \| raw
-rw-r--r--	147	fuzz10.smtv1.smt2	blob \| history \| raw
-rw-r--r--	230	fuzz11.smtv1.smt2	blob \| history \| raw
-rw-r--r--	931	fuzz12.smtv1.smt2	blob \| history \| raw
-rw-r--r--	403	fuzz13.smtv1.smt2	blob \| history \| raw
-rw-r--r--	708	fuzz14.smtv1.smt2	blob \| history \| raw
-rw-r--r--	2146	fuzz15.delta01.smtv1.smt2	blob \| history \| raw
-rw-r--r--	1226	fuzz16.delta01.smtv1.smt2	blob \| history \| raw
-rw-r--r--	1963	fuzz17.delta01.smtv1.smt2	blob \| history \| raw
-rw-r--r--	2429	fuzz18.delta01.smtv1.smt2	blob \| history \| raw
-rw-r--r--	2238	fuzz18.delta02.smtv1.smt2	blob \| history \| raw
-rw-r--r--	634	fuzz18.delta03.smtv1.smt2	blob \| history \| raw
-rw-r--r--	2744	fuzz19.delta01.smtv1.smt2	blob \| history \| raw
-rw-r--r--	287	fuzz20.delta01.smtv1.smt2	blob \| history \| raw
-rw-r--r--	7856	fuzz20.smtv1.smt2	blob \| history \| raw
-rw-r--r--	205	fuzz21.delta01.smtv1.smt2	blob \| history \| raw
-rw-r--r--	25265	fuzz21.smtv1.smt2	blob \| history \| raw
-rw-r--r--	1100	fuzz22.delta01.smtv1.smt2	blob \| history \| raw
-rw-r--r--	5411	fuzz22.smtv1.smt2	blob \| history \| raw
-rw-r--r--	192	fuzz23.delta01.smtv1.smt2	blob \| history \| raw
-rw-r--r--	9755	fuzz23.smtv1.smt2	blob \| history \| raw
-rw-r--r--	231	fuzz24.delta01.smtv1.smt2	blob \| history \| raw
-rw-r--r--	11527	fuzz24.smtv1.smt2	blob \| history \| raw
-rw-r--r--	295	fuzz25.delta01.smtv1.smt2	blob \| history \| raw
-rw-r--r--	16626	fuzz25.smtv1.smt2	blob \| history \| raw
-rw-r--r--	363	fuzz26.delta01.smtv1.smt2	blob \| history \| raw
-rw-r--r--	46366	fuzz26.smtv1.smt2	blob \| history \| raw
-rw-r--r--	236	fuzz27.delta01.smtv1.smt2	blob \| history \| raw
-rw-r--r--	5404	fuzz27.smtv1.smt2	blob \| history \| raw
-rw-r--r--	192	fuzz28.delta01.smtv1.smt2	blob \| history \| raw
-rw-r--r--	18066	fuzz28.smtv1.smt2	blob \| history \| raw
-rw-r--r--	1043	fuzz29.delta01.smtv1.smt2	blob \| history \| raw
-rw-r--r--	3365	fuzz29.smtv1.smt2	blob \| history \| raw
-rw-r--r--	228	fuzz30.delta01.smtv1.smt2	blob \| history \| raw
-rw-r--r--	2355	fuzz30.smtv1.smt2	blob \| history \| raw
-rw-r--r--	264	fuzz31.delta01.smtv1.smt2	blob \| history \| raw
-rw-r--r--	20862	fuzz31.smtv1.smt2	blob \| history \| raw
-rw-r--r--	402	fuzz32.delta01.smtv1.smt2	blob \| history \| raw
-rw-r--r--	63856	fuzz32.smtv1.smt2	blob \| history \| raw
-rw-r--r--	192	fuzz33.delta01.smtv1.smt2	blob \| history \| raw
-rw-r--r--	5501	fuzz33.smtv1.smt2	blob \| history \| raw
-rw-r--r--	377	fuzz34.delta01.smtv1.smt2	blob \| history \| raw
-rw-r--r--	230	fuzz35.delta01.smtv1.smt2	blob \| history \| raw
-rw-r--r--	13828	fuzz35.smtv1.smt2	blob \| history \| raw
-rw-r--r--	822	fuzz36.delta01.smtv1.smt2	blob \| history \| raw
-rw-r--r--	14276	fuzz36.smtv1.smt2	blob \| history \| raw
-rw-r--r--	262	fuzz37.delta01.smtv1.smt2	blob \| history \| raw
-rw-r--r--	4691	fuzz37.smtv1.smt2	blob \| history \| raw
-rw-r--r--	337	fuzz38.delta01.smtv1.smt2	blob \| history \| raw
-rw-r--r--	264	fuzz39.delta01.smtv1.smt2	blob \| history \| raw
-rw-r--r--	4332	fuzz39.smtv1.smt2	blob \| history \| raw
-rw-r--r--	188	fuzz40.delta01.smtv1.smt2	blob \| history \| raw
-rw-r--r--	4591	fuzz40.smtv1.smt2	blob \| history \| raw
-rw-r--r--	8967	fuzz41.smtv1.smt2	blob \| history \| raw
-rw-r--r--	166	incorrect1.delta01.smtv1.smt2	blob \| history \| raw
-rw-r--r--	459	inequality00.smt2	blob \| history \| raw
-rw-r--r--	489	inequality01.smt2	blob \| history \| raw
-rw-r--r--	491	inequality02.smt2	blob \| history \| raw
-rw-r--r--	222	inequality03.smt2	blob \| history \| raw
-rw-r--r--	443	inequality04.smt2	blob \| history \| raw
-rw-r--r--	643	inequality05.smt2	blob \| history \| raw
-rw-r--r--	279	int_to_bv_err_on_demand_1.smt2	blob \| history \| raw
-rw-r--r--	193	int_to_bv_model.smt2	blob \| history \| raw
-rw-r--r--	129	int_to_bv_model2.smt2	blob \| history \| raw
-rw-r--r--	339	issue-4075.smt2	blob \| history \| raw
-rw-r--r--	348	issue-4076.smt2	blob \| history \| raw
-rw-r--r--	369	issue-4130.smt2	blob \| history \| raw
-rw-r--r--	114	issue3621.smt2	blob \| history \| raw
-rw-r--r--	286	issue5396.smt2	blob \| history \| raw
-rw-r--r--	160	issue8159-1-rewrite-bvneg.smt2	blob \| history \| raw
-rw-r--r--	212	issue8240-rewrite-bvnot.smt2	blob \| history \| raw
-rw-r--r--	249	issue8654-bitblast-quant-exc.smt2	blob \| history \| raw
-rw-r--r--	179	mul-neg-unsat.smt2	blob \| history \| raw
-rw-r--r--	198	mul-negpow2.smt2	blob \| history \| raw
-rw-r--r--	151	mult-pow2-negative.smt2	blob \| history \| raw
-rw-r--r--	211	pr4993-bvugt-bvurem-a.smt2	blob \| history \| raw
-rw-r--r--	257	pr4993-bvugt-bvurem-b.smt2	blob \| history \| raw
-rw-r--r--	151	proj-issue343.smt2	blob \| history \| raw
-rw-r--r--	342	proj-issue438-prerewrite-fixed-point.smt2	blob \| history \| raw
-rw-r--r--	413	reset-assertions-assert-input.smt2	blob \| history \| raw
-rw-r--r--	224	sizecheck.cvc.smt2	blob \| history \| raw
-rw-r--r--	418	smtcompbug.smtv1.smt2	blob \| history \| raw
-rw-r--r--	584	test-bv_intro_pow2.smt2	blob \| history \| raw
-rw-r--r--	1083	test00.smtv1.smt2	blob \| history \| raw
-rw-r--r--	319	unsound1-reduced.smt2	blob \| history \| raw