diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2021-06-25 19:42:43 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-25 19:42:43 -0700 |
| commit | eefd31d2fe256bdee9a5c33105eced1a358bb378 (patch) | |
| tree | 5b8d52bdfc288557bf6456ca315ad2862ab4669b /test/regress/regress0/fmf/fc-unsat-pent.smt2 | |
| parent | abd18eeb854047e13e38518c536afd16a1be448d (diff) | |
pow2 -- final changes (#6800)
This commit adds the remaining changes for a working and integrated `pow2` solver.
In particular, it adds a rewrite and a lemma that identify `pow2(x)` with `0` whenever `x<0`.
Regressions are added as well, including `pow2-native-0.smt2` that shows the semantics of `pow2` on negative values.
The next steps are new rewrites and and more lemma schemas.
Diffstat (limited to 'test/regress/regress0/fmf/fc-unsat-pent.smt2')
0 files changed, 0 insertions, 0 deletions