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	246	log plain
-rw-r--r--	crash1220.smt2	337	log plain
-rw-r--r--	dispose-list-4-init.smt2	795	log plain
-rw-r--r--	emp2-quant-unsat.smt2	252	log plain
-rw-r--r--	finite-witness-sat.smt2	244	log plain
-rw-r--r--	fmf-nemp-2.smt2	357	log plain
-rw-r--r--	loop-1220.smt2	552	log plain
-rw-r--r--	pto-04.smt2	756	log plain
-rw-r--r--	quant_wand.smt2	262	log plain
-rw-r--r--	sep-02.smt2	301	log plain
-rw-r--r--	sep-03.smt2	325	log plain
-rw-r--r--	sep-find2.smt2	460	log plain
-rw-r--r--	sep-fmf-priority.smt2	267	log plain
-rw-r--r--	sep-neg-1refine.smt2	347	log plain
-rw-r--r--	sep-neg-nstrict.smt2	267	log plain
-rw-r--r--	sep-neg-nstrict2.smt2	336	log plain
-rw-r--r--	sep-neg-simple.smt2	301	log plain
-rw-r--r--	sep-neg-swap.smt2	318	log plain
-rw-r--r--	sep-nterm-again.smt2	397	log plain
-rw-r--r--	sep-nterm-val-model.smt2	302	log plain
-rw-r--r--	sep-simp-unc.smt2	274	log plain
-rw-r--r--	simple-neg-sat.smt2	365	log plain
-rw-r--r--	sl-standard.smt2	1100	log plain
-rw-r--r--	split-find-unsat-w-emp.smt2	377	log plain
-rw-r--r--	split-find-unsat.smt2	387	log plain
-rw-r--r--	wand-0526-sat.smt2	257	log plain
-rw-r--r--	wand-false.smt2	182	log plain
-rw-r--r--	wand-nterm-simp.smt2	170	log plain
-rw-r--r--	wand-nterm-simp2.smt2	192	log plain
-rw-r--r--	wand-simp-sat.smt2	163	log plain
-rw-r--r--	wand-simp-sat2.smt2	186	log plain
-rw-r--r--	wand-simp-unsat.smt2	172	log plain