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	1071	log plain
-rw-r--r--	aufbv-fuzz01.smt	14997	log plain
-rw-r--r--	aufbv-fuzz01.smt.expect	66	log plain
-rw-r--r--	bitvec0.delta01.smt	460	log plain
-rw-r--r--	bitvec0.delta01.smt.expect	68	log plain
-rw-r--r--	bitvec0.smt	1790	log plain
-rw-r--r--	bitvec0.smt.expect	68	log plain
-rw-r--r--	bitvec5.smt	751	log plain
-rw-r--r--	bitvec5.smt.expect	68	log plain
-rw-r--r--	bug347.smt	541	log plain
-rw-r--r--	bug347.smt.expect	66	log plain
-rw-r--r--	just_sat.expect	66	log plain
-rw-r--r--	just_unsat.expect	68	log plain
-rw-r--r--	quant-Arrays_Q1-noinfer.smt2	4185	log plain
-rw-r--r--	quant-Arrays_Q1-noinfer.smt2.expect	68	log plain
-rw-r--r--	quant-symmetric_unsat_7.smt2	1536	log plain
-rw-r--r--	quant-symmetric_unsat_7.smt2.expect	68	log plain
-rw-r--r--	uflia-error0.smt2	360930	log plain
-rw-r--r--	uflia-error0.smt2.expect	68	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	66	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	68	log plain
-rw-r--r--	wchains010ue.delta02.smt	903	log plain
-rw-r--r--	wchains010ue.delta02.smt.expect	68	log plain
-rw-r--r--	wchains010ue.smt	7461	log plain
-rw-r--r--	wchains010ue.smt.expect	68	log plain