From 166d4351fe55d182a4ed355ac729c5d40a1f9bc1 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 3 Apr 2018 15:49:43 -0500
Subject: Use choice when expanding definitions for inverse transcendental
 functions (#1742)

---
 test/regress/regress1/nl/arctan2-expdef.smt2 | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 test/regress/regress1/nl/arctan2-expdef.smt2

(limited to 'test/regress/regress1/nl')

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)
-- 
cgit v1.2.3