diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-01-31 06:06:39 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-01-31 08:06:39 -0600 |
| commit | b77641f3db3d868536549deb0fc7851ff07b5e88 (patch) | |
| tree | 3377181222efba76be911604e8f179d3c90d7cb9 /test/regress/regress0/arith | |
| parent | a456ef81b15e2f8612cd41a31ad811af35f47846 (diff) | |
Fix arithmetic rewriter for exponential (#3688)
Diffstat (limited to 'test/regress/regress0/arith')
| -rw-r--r-- | test/regress/regress0/arith/issue3683.smt2 | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/test/regress/regress0/arith/issue3683.smt2 b/test/regress/regress0/arith/issue3683.smt2 new file mode 100644 index 000000000..0ce6dc89d --- /dev/null +++ b/test/regress/regress0/arith/issue3683.smt2 @@ -0,0 +1,5 @@ +(set-logic ALL) +(declare-fun a () Real) +(assert (= (+ 2 (exp (+ 2 a))) 0)) +(set-info :status unsat) +(check-sat) |