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--	chain-int.smt2	256	log plain
-rw-r--r--	crash1220.smt2	347	log plain
-rw-r--r--	dispose-list-4-init.smt2	805	log plain
-rw-r--r--	emp2-quant-unsat.smt2	262	log plain
-rw-r--r--	finite-witness-sat.smt2	272	log plain
-rw-r--r--	fmf-nemp-2.smt2	367	log plain
-rw-r--r--	loop-1220.smt2	562	log plain
-rw-r--r--	pto-04.smt2	766	log plain
-rw-r--r--	quant_wand.smt2	272	log plain
-rw-r--r--	sep-02.smt2	311	log plain
-rw-r--r--	sep-03.smt2	335	log plain
-rw-r--r--	sep-find2.smt2	460	log plain
-rw-r--r--	sep-fmf-priority.smt2	295	log plain
-rw-r--r--	sep-neg-1refine.smt2	357	log plain
-rw-r--r--	sep-neg-nstrict.smt2	277	log plain
-rw-r--r--	sep-neg-nstrict2.smt2	346	log plain
-rw-r--r--	sep-neg-simple.smt2	311	log plain
-rw-r--r--	sep-neg-swap.smt2	328	log plain
-rw-r--r--	sep-nterm-again.smt2	407	log plain
-rw-r--r--	sep-nterm-val-model.smt2	312	log plain
-rw-r--r--	sep-simp-unc.smt2	284	log plain
-rw-r--r--	simple-neg-sat.smt2	375	log plain
-rw-r--r--	sl-standard.smt2	1100	log plain
-rw-r--r--	split-find-unsat-w-emp.smt2	387	log plain
-rw-r--r--	split-find-unsat.smt2	415	log plain
-rw-r--r--	wand-0526-sat.smt2	267	log plain
-rw-r--r--	wand-false.smt2	192	log plain
-rw-r--r--	wand-nterm-simp.smt2	180	log plain
-rw-r--r--	wand-nterm-simp2.smt2	202	log plain
-rw-r--r--	wand-simp-sat.smt2	173	log plain
-rw-r--r--	wand-simp-sat2.smt2	196	log plain
-rw-r--r--	wand-simp-unsat.smt2	200	log plain