Add non-linear regressions, disable nlAlgSubs, do not do rep checking for NONLINEAR_MULT terms. Ensure shared terms have correct model values in non-linear solver.

1 files changed, 72 insertions, 0 deletions

diff --git a/test/regress/regress0/nl/magnitude-wrong-1020-m.smt2 b/test/regress/regress0/nl/magnitude-wrong-1020-m.smt2
new file mode 100644
index 000000000..d0c038d73
--- /dev/null
+++ b/test/regress/regress0/nl/magnitude-wrong-1020-m.smt2
@@ -0,0 +1,72 @@
+; COMMAND-LINE: --nl-alg
+; EXPECT: sat
+(set-logic QF_NRA)
+(set-info :source |
+From termination analysis of term rewriting.
+
+Submitted by Harald Roman Zankl <Harald.Zankl@uibk.ac.at>
+
+|)
+(set-info :smt-lib-version 2.0)
+(set-info :category "industrial")
+(set-info :status sat)
+  (define-fun x6 () Real
+    1.0)
+  (define-fun x13 () Real
+    (/ 1.0 32.0))
+  (define-fun x3 () Real
+    1.0)
+  (define-fun x10 () Real
+    1.0)
+  (define-fun x0 () Real
+    1.0)
+  (define-fun x17 () Real
+    3.0)
+  (define-fun x7 () Real
+    (/ 1.0 4.0))
+  (define-fun x14 () Real
+    (/ 3.0 4.0))
+  (define-fun x4 () Real
+    2.0)
+  (define-fun x11 () Real
+    1.0)
+  (define-fun x1 () Real
+    (/ 3.0 2.0))
+  (define-fun x18 () Real
+    0.0)
+  (define-fun x8 () Real
+    1.0)
+  (define-fun x15 () Real
+    1.0)
+  (define-fun x5 () Real
+    1.0)
+  (define-fun x12 () Real
+    2.0)
+  (define-fun x2 () Real
+    1.0)
+  (define-fun x9 () Real
+    0.0)
+  (define-fun x16 () Real
+    (/ 1.0 4.0))
+
+(assert (>= x6 0))
+(assert (>= x13 0))
+(assert (>= x3 0))
+(assert (>= x10 0))
+(assert (>= x0 0))
+(assert (>= x17 0))
+(assert (>= x7 0))
+(assert (>= x14 0))
+(assert (>= x4 0))
+(assert (>= x11 0))
+(assert (>= x1 0))
+(assert (>= x18 0))
+(assert (>= x8 0))
+(assert (>= x15 0))
+(assert (>= x5 0))
+(assert (>= x12 0))
+(assert (>= x2 0))
+(assert (>= x9 0))
+(assert (>= x16 0))
+(assert (let ((?v_0 (+ x0 (* x2 x3))) (?v_2 (* x2 x4)) (?v_1 (+ x5 (* x6 x7))) (?v_4 (* x12 x3))) (let ((?v_3 (+ (+ x10 (* x11 x3)) ?v_4)) (?v_6 (* x11 x4)) (?v_7 (* x12 x4)) (?v_5 (+ (+ x10 (* x11 x7)) ?v_4))) (let ((?v_17 (and (and (and (and (and (> ?v_0 x0) (>= ?v_0 x0)) (>= ?v_2 x2)) (and (and (and (> ?v_0 ?v_1) (>= ?v_0 ?v_1)) (>= x1 (* x6 x8))) (>= ?v_2 (* x6 x9)))) (and (and (and (> ?v_3 x0) (>= ?v_3 x0)) (>= ?v_6 x1)) (>= ?v_7 x2))) (and (and (and (> ?v_3 ?v_5) (>= ?v_3 ?v_5)) (>= ?v_6 (* x11 x8))) (>= ?v_7 (+ (* x11 x9) ?v_7))))) (?v_8 (+ x13 (* x14 x3))) (?v_9 (+ x7 (* x9 x15))) (?v_11 (+ x13 (* x14 x7))) (?v_10 (+ x7 (* x9 x3))) (?v_13 (* x18 x3))) (let ((?v_12 (+ (+ x16 (* x17 x15)) ?v_13)) (?v_15 (+ x3 (* x4 (+ (+ x16 (* x17 x7)) ?v_13)))) (?v_14 (+ (+ x16 (* x17 x3)) ?v_13)) (?v_16 (* x18 x4))) (and (and (and (and (and (and ?v_17 (and (and (> ?v_8 0) (>= ?v_8 0)) (>= (* x14 x4) 1))) (and (and (> ?v_9 0) (>= ?v_9 0)) (>= x8 1))) (and (and (and (> ?v_10 ?v_11) (>= ?v_10 ?v_11)) (>= x8 (* x14 x8))) (>= (* x9 x4) (* x14 x9)))) (and (> ?v_12 x15) (>= ?v_12 x15))) (and (and (and (> ?v_14 ?v_15) (>= ?v_14 ?v_15)) (>= (* x17 x4) (* x4 (* x17 x8)))) (>= ?v_16 (* x4 (+ (* x17 x9) ?v_16))))) ?v_17))))))
+(check-sat)