sep « regress1 « 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	140	log plain
-rw-r--r--	Makefile.am	1438	log plain
-rw-r--r--	chain-int.smt2	231	log plain
-rw-r--r--	crash1220.smt2	322	log plain
-rw-r--r--	dispose-list-4-init.smt2	780	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--	loop-1220.smt2	537	log plain
-rw-r--r--	pto-04.smt2	741	log plain
-rw-r--r--	quant_wand.smt2	241	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-simp-unc.smt2	263	log plain
-rw-r--r--	simple-neg-sat.smt2	350	log plain
-rw-r--r--	split-find-unsat-w-emp.smt2	356	log plain
-rw-r--r--	split-find-unsat.smt2	390	log plain
-rw-r--r--	wand-0526-sat.smt2	236	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