diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-03 15:49:43 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-04-03 15:49:43 -0500 |
| commit | 166d4351fe55d182a4ed355ac729c5d40a1f9bc1 (patch) | |
| tree | 32a136e8963ff487f5ddfb475eea9ae9d020a65d /test/regress/regress1/nl | |
| parent | 77c09d4c79224b726183cfd59df3cf5eff3ff4ea (diff) | |
Use choice when expanding definitions for inverse transcendental functions (#1742)
Diffstat (limited to 'test/regress/regress1/nl')
| -rw-r--r-- | test/regress/regress1/nl/arctan2-expdef.smt2 | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/test/regress/regress1/nl/arctan2-expdef.smt2 b/test/regress/regress1/nl/arctan2-expdef.smt2 new file mode 100644 index 000000000..8a8494873 --- /dev/null +++ b/test/regress/regress1/nl/arctan2-expdef.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_NRA) +(set-info :status unsat) +(set-option :arith-no-partial-fun true) +(declare-fun lat1 () Real) +(declare-fun lat2 () Real) + +(declare-fun arctan2u () Real) +(define-fun arctan2 ((x Real) (y Real)) Real + (arctan (/ y x))) + +(assert (= (arctan2 lat1 lat2) 3)) +(check-sat) |