sep « 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.am	1829	log plain
-rw-r--r--	chain-int.smt2	231	log plain
-rw-r--r--	crash1220.smt2	322	log plain
-rw-r--r--	dispose-1.smt2	389	log plain
-rw-r--r--	dispose-list-4-init.smt2	780	log plain
-rw-r--r--	dup-nemp.smt2	175	log plain
-rw-r--r--	emp2-quant-unsat.smt2	237	log plain
-rw-r--r--	finite-witness-sat.smt2	241	log plain
-rw-r--r--	fmf-nemp-2.smt2	341	log plain
-rw-r--r--	nemp.smt2	114	log plain
-rw-r--r--	nil-no-elim.smt2	175	log plain
-rw-r--r--	nspatial-simp.smt2	216	log plain
-rw-r--r--	pto-01.smt2	195	log plain
-rw-r--r--	pto-02.smt2	486	log plain
-rw-r--r--	pto-04.smt2	741	log plain
-rw-r--r--	quant_wand.smt2	241	log plain
-rw-r--r--	sep-01.smt2	211	log plain
-rw-r--r--	sep-02.smt2	286	log plain
-rw-r--r--	sep-03.smt2	310	log plain
-rw-r--r--	sep-find2.smt2	441	log plain
-rw-r--r--	sep-fmf-priority.smt2	270	log plain
-rw-r--r--	sep-neg-1refine.smt2	332	log plain
-rw-r--r--	sep-neg-nstrict.smt2	252	log plain
-rw-r--r--	sep-neg-nstrict2.smt2	321	log plain
-rw-r--r--	sep-neg-simple.smt2	286	log plain
-rw-r--r--	sep-neg-swap.smt2	303	log plain
-rw-r--r--	sep-nterm-again.smt2	382	log plain
-rw-r--r--	sep-nterm-val-model.smt2	287	log plain
-rw-r--r--	sep-plus1.smt2	299	log plain
-rw-r--r--	sep-simp-unsat-emp.smt2	225	log plain
-rw-r--r--	simple-neg-sat.smt2	350	log plain
-rw-r--r--	trees-1.smt2	1195	log plain
-rw-r--r--	wand-0526-sat.smt2	236	log plain
-rw-r--r--	wand-crash.smt2	125	log plain
-rw-r--r--	wand-false.smt2	167	log plain
-rw-r--r--	wand-nterm-simp.smt2	149	log plain
-rw-r--r--	wand-nterm-simp2.smt2	171	log plain
-rw-r--r--	wand-simp-sat.smt2	148	log plain
-rw-r--r--	wand-simp-sat2.smt2	171	log plain
-rw-r--r--	wand-simp-unsat.smt2	169	log plain