![[ICO]](/icons/blank.gif){kind=icon}
![[PARENTDIR]](/icons/back.gif){kind=icon}
![[TXT]](/icons/text.gif){kind=icon}
| Name | Last modified | Size | Description |
|---|---|---|---|---|
| Parent Directory | - | ||
| NAVIGATION2.smt2 | 2024-09-15 02:50 | 681 | |
| approx-sqrt-unsat.smt2 | 2024-09-15 02:50 | 368 | |
| approx-sqrt.smt2 | 2024-09-15 02:50 | 331 | |
| arctan2-expdef.smt2 | 2024-09-15 02:50 | 290 | |
| arrowsmith-050317.smt2 | 2024-09-15 02:50 | 14K | |
| bad-050217.smt2 | 2024-09-15 02:50 | 2.8K | |
| bug698.smt2 | 2024-09-15 02:50 | 768 | |
| coeff-unsat-base.smt2 | 2024-09-15 02:50 | 244 | |
| coeff-unsat.smt2 | 2024-09-15 02:50 | 244 | |
| combine.smt2 | 2024-09-15 02:50 | 241 | |
| cos-bound.smt2 | 2024-09-15 02:50 | 129 | |
| cos1-tc.smt2 | 2024-09-15 02:50 | 178 | |
| disj-eval.smt2 | 2024-09-15 02:50 | 281 | |
| dist-big.smt2 | 2024-09-15 02:50 | 431 | |
| div-mod-partial.smt2 | 2024-09-15 02:50 | 311 | |
| dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2 | 2024-09-15 02:50 | 4.9K | |
| exp-4.5-lt.smt2 | 2024-09-15 02:50 | 157 | |
| exp-approx.smt2 | 2024-09-15 02:50 | 475 | |
| exp-soundness-bound.smt2 | 2024-09-15 02:50 | 153 | |
| exp1-lb.smt2 | 2024-09-15 02:50 | 185 | |
| exp_monotone.smt2 | 2024-09-15 02:50 | 309 | |
| ext-rew-aggr-test.smt2 | 2024-09-15 02:50 | 8.5K | |
| factor_agg_s.smt2 | 2024-09-15 02:50 | 905 | |
| iand-native-2.smt2 | 2024-09-15 02:50 | 421 | |
| iand-native-granularities.smt2 | 2024-09-15 02:50 | 618 | |
| issue3300-approx-sqrt-witness.smt2 | 2024-09-15 02:50 | 306 | |
| issue3307.smt2 | 2024-09-15 02:50 | 209 | |
| issue3441.smt2 | 2024-09-15 02:50 | 561 | |
| issue3617.smt2 | 2024-09-15 02:50 | 538 | |
| issue3647.smt2 | 2024-09-15 02:50 | 175 | |
| issue3656.smt2 | 2024-09-15 02:50 | 235 | |
| issue3803-nl-check-model.smt2 | 2024-09-15 02:50 | 359 | |
| issue3955-ee-double-notify.smt2 | 2024-09-15 02:50 | 181 | |
| issue3966-conf-coeff.smt2 | 2024-09-15 02:50 | 690 | |
| issue4334-sat-proof.smt2 | 2024-09-15 02:50 | 31K | |
| issue4791-llr.smt2 | 2024-09-15 02:50 | 489 | |
| issue5372-2-no-m-presolve.smt2 | 2024-09-15 02:50 | 263 | |
| issue5461-iand-init-refine.smt2 | 2024-09-15 02:50 | 211 | |
| issue5660-mb-success.smt2 | 2024-09-15 02:50 | 787 | |
| issue5662-nl-tc-min.smt2 | 2024-09-15 02:50 | 275 | |
| issue5662-nl-tc.smt2 | 2024-09-15 02:50 | 528 | |
| issue7924-sqrt-partial.smt2 | 2024-09-15 02:50 | 146 | |
| issue7948-3-unsound-sin-region.smt2 | 2024-09-15 02:50 | 170 | |
| issue8016-iand-rewrite.smt2 | 2024-09-15 02:50 | 141 | |
| issue8052-iand-rewrite.smt2 | 2024-09-15 02:50 | 141 | |
| issue8118-elim-sin.smt2 | 2024-09-15 02:50 | 257 | |
| issue8162-drop-pi-bound.smt2 | 2024-09-15 02:50 | 218 | |
| learned-rewrite-int-mod-range.smt2 | 2024-09-15 02:50 | 561 | |
| metitarski-3-4.smt2 | 2024-09-15 02:50 | 1.3K | |
| metitarski-1025.smt2 | 2024-09-15 02:50 | 1.0K | |
| metitarski_3_4_2e.smt2 | 2024-09-15 02:50 | 1.4K | |
| mirko-050417.smt2 | 2024-09-15 02:50 | 8.7K | |
| nl-eq-infer.smt2 | 2024-09-15 02:50 | 283 | |
| nl-help-unsat-quant.smt2 | 2024-09-15 02:50 | 31K | |
| nl-unk-quant.smt2 | 2024-09-15 02:50 | 1.2K | |
| nl_uf_lalt.smt2 | 2024-09-15 02:50 | 276 | |
| nra-cad-performance.smt2 | 2024-09-15 02:50 | 1.1K | |
| ones.smt2 | 2024-09-15 02:50 | 346 | |
| pinto-model-core-ni.smt2 | 2024-09-15 02:50 | 685 | |
| poly-1025.smt2 | 2024-09-15 02:50 | 1.5K | |
| proj-365-is-int-pi.smt2 | 2024-09-15 02:50 | 106 | |
| proj-issue215.smt2 | 2024-09-15 02:50 | 287 | |
| proj-issue231.smt2 | 2024-09-15 02:50 | 213 | |
| proj-issue232.smt2 | 2024-09-15 02:50 | 301 | |
| proj-issue251.smt2 | 2024-09-15 02:50 | 483 | |
| proj-issue253.smt2 | 2024-09-15 02:50 | 236 | |
| proj-issue279.smt2 | 2024-09-15 02:50 | 146 | |
| proj-issue280.smt2 | 2024-09-15 02:50 | 154 | |
| proj-issue282.smt2 | 2024-09-15 02:50 | 202 | |
| proj-issue286.smt2 | 2024-09-15 02:50 | 228 | |
| proj-issue290.smt2 | 2024-09-15 02:50 | 141 | |
| proj-issue291.smt2 | 2024-09-15 02:50 | 176 | |
| proj-issue292.smt2 | 2024-09-15 02:50 | 207 | |
| proj-issue294.smt2 | 2024-09-15 02:50 | 109 | |
| proj-issue297.smt2 | 2024-09-15 02:50 | 150 | |
| proj-issue302.smt2 | 2024-09-15 02:50 | 125 | |
| quant-nl.smt2 | 2024-09-15 02:50 | 73K | |
| red-exp.smt2 | 2024-09-15 02:50 | 241 | |
| rewriting-sums.smt2 | 2024-09-15 02:50 | 332 | |
| shifting.smt2 | 2024-09-15 02:50 | 353 | |
| shifting2.smt2 | 2024-09-15 02:50 | 385 | |
| simple-mono-unsat.smt2 | 2024-09-15 02:50 | 296 | |
| simple-mono.smt2 | 2024-09-15 02:50 | 278 | |
| sin-compare-across-phase.smt2 | 2024-09-15 02:50 | 179 | |
| sin-compare.smt2 | 2024-09-15 02:50 | 209 | |
| sin-init-tangents.smt2 | 2024-09-15 02:50 | 180 | |
| sin-sign.smt2 | 2024-09-15 02:50 | 207 | |
| sin-sym2.smt2 | 2024-09-15 02:50 | 293 | |
| sin1-deq-sat.smt2 | 2024-09-15 02:50 | 359 | |
| sin1-lb.smt2 | 2024-09-15 02:50 | 185 | |
| sin1-sat.smt2 | 2024-09-15 02:50 | 274 | |
| sin1-ub.smt2 | 2024-09-15 02:50 | 186 | |
| sin2-lb.smt2 | 2024-09-15 02:50 | 184 | |
| sin2-ub.smt2 | 2024-09-15 02:50 | 185 | |
| solve-eq-small-qf-nra.smt2 | 2024-09-15 02:50 | 457 | |
| sqrt-problem-1.smt2 | 2024-09-15 02:50 | 1.4K | |
| sugar-ident-2.smt2 | 2024-09-15 02:50 | 560 | |
| sugar-ident-3.smt2 | 2024-09-15 02:50 | 194 | |
| sugar-ident.smt2 | 2024-09-15 02:50 | 547 | |
| tan-rewrite2.smt2 | 2024-09-15 02:50 | 242 | |
| transcedental_model_simple.smt2 | 2024-09-15 02:50 | 171 | |
| zero-subset.smt2 | 2024-09-15 02:50 | 287 | |