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	351	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	14138	log plain
-rw-r--r--	bad-050217.smt2	2855	log plain
-rw-r--r--	bug698.smt2	757	log plain
-rw-r--r--	coeff-unsat-base.smt2	239	log plain
-rw-r--r--	coeff-unsat.smt2	239	log plain
-rw-r--r--	combine.smt2	236	log plain
-rw-r--r--	cos-bound.smt2	124	log plain
-rw-r--r--	cos1-tc.smt2	177	log plain
-rw-r--r--	disj-eval.smt2	276	log plain
-rw-r--r--	dist-big.smt2	426	log plain
-rw-r--r--	div-mod-partial.smt2	306	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	163	log plain
-rw-r--r--	exp1-lb.smt2	185	log plain
-rw-r--r--	exp_monotone.smt2	304	log plain
-rw-r--r--	ext-rew-aggr-test.smt2	8708	log plain
-rw-r--r--	factor_agg_s.smt2	822	log plain
-rw-r--r--	iand-native-1.smt2	696	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	186	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--	issue5372-2-no-m-presolve.smt2	263	log plain
-rw-r--r--	issue5662-nl-tc-min.smt2	275	log plain
-rw-r--r--	issue5662-nl-tc.smt2	496	log plain
-rw-r--r--	metitarski-1025.smt2	1046	log plain
-rw-r--r--	metitarski-3-4.smt2	1350	log plain
-rw-r--r--	metitarski_3_4_2e.smt2	1419	log plain
-rw-r--r--	mirko-050417.smt2	8914	log plain
-rw-r--r--	nl-eq-infer.smt2	283	log plain
-rw-r--r--	nl-help-unsat-quant.smt2	31573	log plain
-rw-r--r--	nl-unk-quant.smt2	1173	log plain
-rw-r--r--	nl_uf_lalt.smt2	299	log plain
-rw-r--r--	ones.smt2	341	log plain
-rw-r--r--	pinto-model-core-ni.smt2	597	log plain
-rw-r--r--	poly-1025.smt2	1516	log plain
-rw-r--r--	quant-nl.smt2	74567	log plain
-rw-r--r--	red-exp.smt2	236	log plain
-rw-r--r--	rewriting-sums.smt2	327	log plain
-rw-r--r--	shifting.smt2	334	log plain
-rw-r--r--	shifting2.smt2	368	log plain
-rw-r--r--	simple-mono-unsat.smt2	291	log plain
-rw-r--r--	simple-mono.smt2	273	log plain
-rw-r--r--	sin-compare-across-phase.smt2	174	log plain
-rw-r--r--	sin-compare.smt2	204	log plain
-rw-r--r--	sin-init-tangents.smt2	175	log plain
-rw-r--r--	sin-sign.smt2	202	log plain
-rw-r--r--	sin-sym2.smt2	288	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	237	log plain
-rw-r--r--	ufnia-factor-open-proof.smt2	502	log plain
-rw-r--r--	zero-subset.smt2	282	log plain