rels « 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--	addr_book_0.cvc.smt2	1725	log plain
-rw-r--r--	atom_univ2.cvc.smt2	604	log plain
-rw-r--r--	card_transpose.cvc.smt2	156	log plain
-rw-r--r--	iden_0.cvc.smt2	713	log plain
-rw-r--r--	iden_1.cvc.smt2	522	log plain
-rw-r--r--	join-eq-u-sat.cvc.smt2	488	log plain
-rw-r--r--	join-eq-u.cvc.smt2	490	log plain
-rw-r--r--	joinImg_0.cvc.smt2	839	log plain
-rw-r--r--	oneLoc_no_quant-int_0_1.cvc.smt2	560	log plain
-rw-r--r--	rel_1tup_0.cvc.smt2	471	log plain
-rw-r--r--	rel_complex_0.cvc.smt2	639	log plain
-rw-r--r--	rel_complex_1.cvc.smt2	765	log plain
-rw-r--r--	rel_conflict_0.cvc.smt2	244	log plain
-rw-r--r--	rel_join_0.cvc.smt2	608	log plain
-rw-r--r--	rel_join_0_1.cvc.smt2	634	log plain
-rw-r--r--	rel_join_1.cvc.smt2	744	log plain
-rw-r--r--	rel_join_1_1.cvc.smt2	731	log plain
-rw-r--r--	rel_join_2.cvc.smt2	452	log plain
-rw-r--r--	rel_join_2_1.cvc.smt2	444	log plain
-rw-r--r--	rel_join_3.cvc.smt2	761	log plain
-rw-r--r--	rel_join_3_1.cvc.smt2	753	log plain
-rw-r--r--	rel_join_4.cvc.smt2	813	log plain
-rw-r--r--	rel_join_5.cvc.smt2	550	log plain
-rw-r--r--	rel_join_6.cvc.smt2	399	log plain
-rw-r--r--	rel_join_7.cvc.smt2	676	log plain
-rw-r--r--	rel_product_0.cvc.smt2	492	log plain
-rw-r--r--	rel_product_0_1.cvc.smt2	484	log plain
-rw-r--r--	rel_product_1.cvc.smt2	528	log plain
-rw-r--r--	rel_product_1_1.cvc.smt2	481	log plain
-rw-r--r--	rel_symbolic_1.cvc.smt2	513	log plain
-rw-r--r--	rel_symbolic_1_1.cvc.smt2	430	log plain
-rw-r--r--	rel_symbolic_2_1.cvc.smt2	471	log plain
-rw-r--r--	rel_symbolic_3_1.cvc.smt2	482	log plain
-rw-r--r--	rel_tc_11.cvc.smt2	520	log plain
-rw-r--r--	rel_tc_2_1.cvc.smt2	694	log plain
-rw-r--r--	rel_tc_3.cvc.smt2	518	log plain
-rw-r--r--	rel_tc_3_1.cvc.smt2	430	log plain
-rw-r--r--	rel_tc_7.cvc.smt2	287	log plain
-rw-r--r--	rel_tc_8.cvc.smt2	255	log plain
-rw-r--r--	rel_tp_3_1.cvc.smt2	382	log plain
-rw-r--r--	rel_tp_join_0.cvc.smt2	825	log plain
-rw-r--r--	rel_tp_join_1.cvc.smt2	758	log plain
-rw-r--r--	rel_tp_join_2.cvc.smt2	562	log plain
-rw-r--r--	rel_tp_join_3.cvc.smt2	762	log plain
-rw-r--r--	rel_tp_join_eq_0.cvc.smt2	661	log plain
-rw-r--r--	rel_tp_join_int_0.cvc.smt2	559	log plain
-rw-r--r--	rel_tp_join_pro_0.cvc.smt2	586	log plain
-rw-r--r--	rel_tp_join_var_0.cvc.smt2	665	log plain
-rw-r--r--	rel_transpose_0.cvc.smt2	404	log plain
-rw-r--r--	rel_transpose_1.cvc.smt2	372	log plain
-rw-r--r--	rel_transpose_1_1.cvc.smt2	416	log plain
-rw-r--r--	rel_transpose_3.cvc.smt2	369	log plain
-rw-r--r--	rel_transpose_4.cvc.smt2	297	log plain
-rw-r--r--	rel_transpose_5.cvc.smt2	511	log plain
-rw-r--r--	rel_transpose_6.cvc.smt2	534	log plain
-rw-r--r--	rel_transpose_7.cvc.smt2	223	log plain
-rw-r--r--	relations-ops.smt2	858	log plain
-rw-r--r--	rels-sharing-simp.cvc.smt2	320	log plain