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 | |
| parent | 77c09d4c79224b726183cfd59df3cf5eff3ff4ea (diff) | |
Use choice when expanding definitions for inverse transcendental functions (#1742)
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/Makefile.tests | 1 | ||||
| -rw-r--r-- | test/regress/regress1/nl/arctan2-expdef.smt2 | 12 |
2 files changed, 13 insertions, 0 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 7f333007a..c3d02bbd6 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1087,6 +1087,7 @@ REG1_TESTS = \ regress1/lemmas/pursuit-safety-8.smt \ regress1/lemmas/simple_startup_9nodes.abstract.base.smt \ regress1/nl/NAVIGATION2.smt2 \ + regress1/nl/arctan2-expdef.smt2 \ regress1/nl/arrowsmith-050317.smt2 \ regress1/nl/bad-050217.smt2 \ regress1/nl/bug698.smt2 \ 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) |