nl « 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--	NAVIGATION2.smt2	681	log plain
-rw-r--r--	approx-sqrt-unsat.smt2	386	log plain
-rw-r--r--	approx-sqrt.smt2	348	log plain
-rw-r--r--	arctan2-expdef.smt2	290	log plain
-rw-r--r--	arrowsmith-050317.smt2	14143	log plain
-rw-r--r--	bad-050217.smt2	2860	log plain
-rw-r--r--	bug698.smt2	762	log plain
-rw-r--r--	coeff-unsat-base.smt2	244	log plain
-rw-r--r--	coeff-unsat.smt2	244	log plain
-rw-r--r--	combine.smt2	241	log plain
-rw-r--r--	cos-bound.smt2	129	log plain
-rw-r--r--	cos1-tc.smt2	182	log plain
-rw-r--r--	disj-eval.smt2	281	log plain
-rw-r--r--	dist-big.smt2	431	log plain
-rw-r--r--	div-mod-partial.smt2	311	log plain
-rw-r--r--	dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2	4991	log plain
-rw-r--r--	exp-4.5-lt.smt2	157	log plain
-rw-r--r--	exp-approx.smt2	490	log plain
-rw-r--r--	exp-soundness-bound.smt2	168	log plain
-rw-r--r--	exp1-lb.smt2	185	log plain
-rw-r--r--	exp_monotone.smt2	309	log plain
-rw-r--r--	ext-rew-aggr-test.smt2	8708	log plain
-rw-r--r--	factor_agg_s.smt2	903	log plain
-rw-r--r--	iand-native-2.smt2	421	log plain
-rw-r--r--	iand-native-granularities.smt2	618	log plain
-rw-r--r--	issue3300-approx-sqrt-witness.smt2	337	log plain
-rw-r--r--	issue3307.smt2	209	log plain
-rw-r--r--	issue3441.smt2	561	log plain
-rw-r--r--	issue3617.smt2	536	log plain
-rw-r--r--	issue3647.smt2	190	log plain
-rw-r--r--	issue3656.smt2	231	log plain
-rw-r--r--	issue3803-nl-check-model.smt2	349	log plain
-rw-r--r--	issue3955-ee-double-notify.smt2	181	log plain
-rw-r--r--	issue3966-conf-coeff.smt2	690	log plain
-rw-r--r--	issue4791-llr.smt2	458	log plain
-rw-r--r--	issue5372-2-no-m-presolve.smt2	263	log plain
-rw-r--r--	issue5660-mb-success.smt2	787	log plain
-rw-r--r--	issue5662-nl-tc-min.smt2	275	log plain
-rw-r--r--	issue5662-nl-tc.smt2	528	log plain
-rw-r--r--	metitarski-1025.smt2	1051	log plain
-rw-r--r--	metitarski-3-4.smt2	1355	log plain
-rw-r--r--	metitarski_3_4_2e.smt2	1424	log plain
-rw-r--r--	mirko-050417.smt2	8919	log plain
-rw-r--r--	nl-eq-infer.smt2	283	log plain
-rw-r--r--	nl-help-unsat-quant.smt2	31578	log plain
-rw-r--r--	nl-unk-quant.smt2	1178	log plain
-rw-r--r--	nl_uf_lalt.smt2	276	log plain
-rw-r--r--	nra-cad-performance.smt2	1143	log plain
-rw-r--r--	ones.smt2	346	log plain
-rw-r--r--	pinto-model-core-ni.smt2	597	log plain
-rw-r--r--	poly-1025.smt2	1521	log plain
-rw-r--r--	quant-nl.smt2	74572	log plain
-rw-r--r--	red-exp.smt2	241	log plain
-rw-r--r--	rewriting-sums.smt2	332	log plain
-rw-r--r--	shifting.smt2	339	log plain
-rw-r--r--	shifting2.smt2	373	log plain
-rw-r--r--	simple-mono-unsat.smt2	296	log plain
-rw-r--r--	simple-mono.smt2	278	log plain
-rw-r--r--	sin-compare-across-phase.smt2	179	log plain
-rw-r--r--	sin-compare.smt2	209	log plain
-rw-r--r--	sin-init-tangents.smt2	180	log plain
-rw-r--r--	sin-sign.smt2	207	log plain
-rw-r--r--	sin-sym2.smt2	293	log plain
-rw-r--r--	sin1-deq-sat.smt2	374	log plain
-rw-r--r--	sin1-lb.smt2	185	log plain
-rw-r--r--	sin1-sat.smt2	289	log plain
-rw-r--r--	sin1-ub.smt2	186	log plain
-rw-r--r--	sin2-lb.smt2	184	log plain
-rw-r--r--	sin2-ub.smt2	185	log plain
-rw-r--r--	solve-eq-small-qf-nra.smt2	474	log plain
-rw-r--r--	sqrt-problem-1.smt2	1479	log plain
-rw-r--r--	sugar-ident-2.smt2	560	log plain
-rw-r--r--	sugar-ident-3.smt2	194	log plain
-rw-r--r--	sugar-ident.smt2	503	log plain
-rw-r--r--	tan-rewrite2.smt2	242	log plain
-rw-r--r--	zero-subset.smt2	287	log plain