From 216f3c9fb07a08909942b91a2a4739cd178f5a72 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 15 Mar 2021 14:08:03 -0500
Subject: Make nonlinear extension account for relevant term set (#6147)

This fixes a subtle issue with non-linear and theory combination.

It currently could use irrelevant terms preregistered to the ExtTheory for its model-based refinement. This means that the non-linear extension could accidentally modify values for terms that are not included in its term set, violating theory combination.

In particular, in the minimized example from #5662, (* a k) was a stale term in ExtTheory, and non-linear extension falsely believed that a was a term whose model value could be modified, since moreover a was not a shared term. In reality, a was not a shared term since it only was registered to UF.

Fixes #5662.
---
 test/regress/CMakeLists.txt                       |  2 ++
 test/regress/regress1/nl/issue5662-nl-tc-min.smt2 | 16 ++++++++++++++++
 test/regress/regress1/nl/issue5662-nl-tc.smt2     | 17 +++++++++++++++++
 3 files changed, 35 insertions(+)
 create mode 100644 test/regress/regress1/nl/issue5662-nl-tc-min.smt2
 create mode 100644 test/regress/regress1/nl/issue5662-nl-tc.smt2

(limited to 'test/regress')

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 30cdf43d9..5c28a34cc 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1596,6 +1596,8 @@ set(regress_1_tests
   regress1/nl/issue3803-nl-check-model.smt2
   regress1/nl/issue3955-ee-double-notify.smt2
   regress1/nl/issue5372-2-no-m-presolve.smt2
+  regress1/nl/issue5662-nl-tc.smt2
+  regress1/nl/issue5662-nl-tc-min.smt2
   regress1/nl/metitarski-1025.smt2
   regress1/nl/metitarski-3-4.smt2
   regress1/nl/metitarski_3_4_2e.smt2
diff --git a/test/regress/regress1/nl/issue5662-nl-tc-min.smt2 b/test/regress/regress1/nl/issue5662-nl-tc-min.smt2
new file mode 100644
index 000000000..0e7279ef9
--- /dev/null
+++ b/test/regress/regress1/nl/issue5662-nl-tc-min.smt2
@@ -0,0 +1,16 @@
+(set-logic NRA)
+(set-info :status sat)
+(declare-fun a () Real)
+(declare-fun j () Real)
+(declare-fun k () Real)
+(declare-fun h () Real)
+(assert (< 0 k))
+(assert (= 1 (* k j)))
+(assert
+    (or
+        (= h 0)
+        (= 0.0 (* a k))
+    )
+)
+(assert (distinct a h))
+(check-sat)
diff --git a/test/regress/regress1/nl/issue5662-nl-tc.smt2 b/test/regress/regress1/nl/issue5662-nl-tc.smt2
new file mode 100644
index 000000000..d805b721d
--- /dev/null
+++ b/test/regress/regress1/nl/issue5662-nl-tc.smt2
@@ -0,0 +1,17 @@
+(set-logic NRA)
+(set-info :status sat)
+(declare-fun a () Real)
+(declare-fun b () Real)
+(declare-fun c () Real)
+(declare-fun d () Real)
+(declare-fun j () Real)
+(declare-fun e () Real)
+(declare-fun f () Real)
+(declare-fun k () Real)
+(declare-fun g () Real)
+(declare-fun h () Real)
+(assert (forall ((i Real)) (xor (and (or (and (or (and (or (and (or
+  (and (> 0.0 (* a e) (* c e)) (>= 0 k)) (<= g 0)) (= (* b j)
+  2.0))))) (> f k)) (>= 0.0 k))) (>= 0 k))))
+(assert (distinct a (* d h)))
+(check-sat)
-- 
cgit v1.2.3