| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | arrowsmith-050317.smt2 | 14137 | logplain |
| -rw-r--r-- | bad-050217.smt2 | 2854 | logplain |
| -rw-r--r-- | cos-bound.smt2 | 123 | logplain |
| -rw-r--r-- | cos-sig-value.smt2 | 156 | logplain |
| -rw-r--r-- | cos1-tc.smt2 | 132 | logplain |
| -rw-r--r-- | dumortier-050317.smt2 | 11594 | logplain |
| -rw-r--r-- | exp_monotone.smt2 | 303 | logplain |
| -rw-r--r-- | shifting.smt2 | 334 | logplain |
| -rw-r--r-- | shifting2.smt2 | 368 | logplain |
| -rw-r--r-- | sin-compare-across-phase.smt2 | 173 | logplain |
| -rw-r--r-- | sin-compare.smt2 | 203 | logplain |
| -rw-r--r-- | sin-init-tangents.smt2 | 174 | logplain |
| -rw-r--r-- | sin-sign.smt2 | 201 | logplain |
| -rw-r--r-- | sin-sym.smt2 | 191 | logplain |
| -rw-r--r-- | sin-sym2.smt2 | 287 | logplain |
| -rw-r--r-- | tan-rewrite.smt2 | 201 | logplain |
| -rw-r--r-- | tan-rewrite2.smt2 | 236 | logplain |
 |
index : cvc5.git | |
| CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. | git repository hosting |
| summaryrefslogtreecommitdiff |
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback