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	1835	log plain
-rw-r--r--	chain-int.smt2	231	log plain
-rwxr-xr-x	crash1220.smt2	322	log plain
-rw-r--r--	dispose-1.smt2	387	log plain
-rw-r--r--	dispose-list-4-init.smt2	780	log plain
-rw-r--r--	dup-nemp.smt2	171	log plain
-rw-r--r--	emp2-quant-unsat.smt2	233	log plain
-rw-r--r--	fmf-nemp-2.smt2	339	log plain
-rw-r--r--	loop-1220.smt2	537	log plain
-rw-r--r--	nemp.smt2	112	log plain
-rwxr-xr-x	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	228	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-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
-rwxr-xr-x	sep-simp-unc.smt2	263	log plain
-rw-r--r--	sep-simp-unsat-emp.smt2	223	log plain
-rw-r--r--	simple-neg-sat.smt2	350	log plain
-rw-r--r--	split-find-unsat-w-emp.smt2	354	log plain
-rw-r--r--	split-find-unsat.smt2	390	log plain
-rw-r--r--	trees-1.smt2	1127	log plain
-rw-r--r--	wand-0526-sat.smt2	234	log plain
-rw-r--r--	wand-crash.smt2	121	log plain
-rw-r--r--	wand-false.smt2	167	log plain
-rw-r--r--	wand-nterm-simp.smt2	147	log plain
-rw-r--r--	wand-nterm-simp2.smt2	169	log plain
-rwxr-xr-x	wand-simp-sat.smt2	148	log plain
-rwxr-xr-x	wand-simp-sat2.smt2	171	log plain
-rwxr-xr-x	wand-simp-unsat.smt2	167	log plain