From 23eb6c0ab05b6607c14ee33b5c0101381aa0bc41 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 11 Dec 2019 11:58:53 -0600
Subject: Do not substitute beneath arithmetic terms in the non-linear solver
 (#3324)

---
 test/regress/CMakeLists.txt             |  1 +
 test/regress/regress1/nl/issue3307.smt2 | 14 ++++++++++++++
 2 files changed, 15 insertions(+)
 create mode 100644 test/regress/regress1/nl/issue3307.smt2

(limited to 'test/regress')

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index edc44c3d2..814eaab49 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1264,6 +1264,7 @@ set(regress_1_tests
   regress1/nl/exp1-lb.smt2
   regress1/nl/exp_monotone.smt2
   regress1/nl/factor_agg_s.smt2
+  regress1/nl/issue3307.smt2
   regress1/nl/issue3441.smt2
   regress1/nl/metitarski-1025.smt2
   regress1/nl/metitarski-3-4.smt2
diff --git a/test/regress/regress1/nl/issue3307.smt2 b/test/regress/regress1/nl/issue3307.smt2
new file mode 100644
index 000000000..803bfeb3a
--- /dev/null
+++ b/test/regress/regress1/nl/issue3307.smt2
@@ -0,0 +1,14 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic NRA)
+(set-info :status sat)
+(declare-fun a () Real)
+(declare-fun b () Real)
+(assert
+ (and
+  (> b 1)
+  (< a 0)
+  (>= (/ 0 (+ (* a b) (/ (- a) 0))) a)
+  )
+ )
+(check-sat)
-- 
cgit v1.2.3