decision « regress0 « regress « test - cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Mode	Name	Size
-rw-r--r--	Makefile	145	log plain
-rw-r--r--	Makefile.am	1644	log plain
-rw-r--r--	aufbv-fuzz01.smt	14997	log plain
-rw-r--r--	aufbv-fuzz01.smt.expect	55	log plain
-rw-r--r--	bitvec0.delta01.smt	460	log plain
-rw-r--r--	bitvec0.delta01.smt.expect	57	log plain
-rw-r--r--	bitvec0.smt	1790	log plain
-rw-r--r--	bitvec0.smt.expect	57	log plain
-rw-r--r--	bitvec5.smt	751	log plain
-rw-r--r--	bitvec5.smt.expect	57	log plain
-rw-r--r--	bug347.smt	541	log plain
-rw-r--r--	bug347.smt.expect	55	log plain
-rw-r--r--	bug374a.smt	38557	log plain
-rw-r--r--	bug374a.smt.expect	57	log plain
-rw-r--r--	bug374b.smt2	602	log plain
-rw-r--r--	bug374b.smt2.expect	76	log plain
-rw-r--r--	error122.delta01.smt	408	log plain
-rw-r--r--	error122.smt	1915	log plain
-rw-r--r--	error20.delta01.smt	392	log plain
-rw-r--r--	error20.smt	2362	log plain
-rw-r--r--	error3.delta01.smt	786	log plain
-rw-r--r--	just_sat.expect	55	log plain
-rw-r--r--	just_unsat.expect	57	log plain
-rw-r--r--	pp-regfile.delta01.smt	959	log plain
-rw-r--r--	pp-regfile.delta01.smt.expect	57	log plain
-rw-r--r--	pp-regfile.delta02.smt	965	log plain
-rw-r--r--	pp-regfile.delta02.smt.expect	57	log plain
-rw-r--r--	quant-ex1.smt2	318	log plain
-rw-r--r--	quant-ex1.smt2.expect	55	log plain
-rw-r--r--	uflia-xs-09-16-3-4-1-5.delta03.smt	1107	log plain
-rw-r--r--	uflia-xs-09-16-3-4-1-5.delta03.smt.expect	55	log plain
-rw-r--r--	uflia-xs-09-16-3-4-1-5.smt	6759	log plain
-rw-r--r--	uflia-xs-09-16-3-4-1-5.smt.expect	57	log plain
-rw-r--r--	wchains010ue.delta02.smt	903	log plain
-rw-r--r--	wchains010ue.delta02.smt.expect	57	log plain
-rw-r--r--	wchains010ue.smt	7461	log plain
-rw-r--r--	wchains010ue.smt.expect	57	log plain