From f7fe461eb8e688547864c7ef6f683192fe89b929 Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Mon, 27 Jul 2026 08:21:56 -0700
Subject: [PATCH] euf_arith_plugin: implement uminus instead of
 NOT_IMPLEMENTED_YET (#10243)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

`euf-completion` crashed with an assertion violation on any unary
negation of a nonlinear product (e.g. `(= (- (* a a)) a)`), because
`register_node` hit `NOT_IMPLEMENTED_YET()` in the `is_uminus` branch.

## Changes

- **`src/ast/euf/euf_arith_plugin.cpp`**: Replace
`NOT_IMPLEMENTED_YET()` with the natural rewrite `-x ↦ (-1) * x`,
consistent with how subtraction is already handled (`x - y ↦ x + (-1 *
y)`). Creates the `-1` numeral of the correct sort, builds the
multiplication enode, and merges via `push_merge`.

- **`src/test/euf_arith_plugin.cpp`**: Add `test4` exercising the exact
repro shape — negation of a nonlinear product merged with a variable.

```smt2
(declare-const a Real)
(set-simplifier euf-completion)
(assert (= (- (* a a)) a))
(check-sat)  ; previously: ASSERTION VIOLATION — now: sat
```

<!-- START COPILOT CODING AGENT SUFFIX -->

- Fixes #10240

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
---
 src/ast/euf/euf_arith_plugin.cpp |  8 +++++++-
 src/test/euf_arith_plugin.cpp    | 21 +++++++++++++++++++++
 2 files changed, 28 insertions(+), 1 deletion(-)

diff --git a/src/ast/euf/euf_arith_plugin.cpp b/src/ast/euf/euf_arith_plugin.cpp
index 82ce7f2a91..59743a4436 100644
--- a/src/ast/euf/euf_arith_plugin.cpp
+++ b/src/ast/euf/euf_arith_plugin.cpp
@@ -78,7 +78,13 @@ namespace euf {
             push_merge(n, n1);
         }
         if (a.is_uminus(e, x)) {
-            NOT_IMPLEMENTED_YET();
+            // -x = -1 * x
+            auto e1 = a.mk_numeral(rational(-1), a.is_int(x));
+            auto n1 = g.find(e1) ? g.find(e1) : g.mk(e1, 0, 0, nullptr);
+            auto e2 = a.mk_mul(e1, x);
+            enode* es1[2] = { n1, g.find(x) };
+            auto mul = g.find(e2) ? g.find(e2) : g.mk(e2, 0, 2, es1);
+            push_merge(n, mul);
         }
 
     }
diff --git a/src/test/euf_arith_plugin.cpp b/src/test/euf_arith_plugin.cpp
index 596db671b4..32da4727ea 100644
--- a/src/test/euf_arith_plugin.cpp
+++ b/src/test/euf_arith_plugin.cpp
@@ -98,9 +98,30 @@ static void test3() {
     std::cout << g << "\n";
 }
 
+static void test4() {
+    ast_manager m;
+    reg_decl_plugins(m);
+    euf::egraph g(m);
+    g.add_plugin(alloc(euf::arith_plugin, g));
+    arith_util a(m);
+    sort_ref R(a.mk_real(), m);
+
+    // Test that -(a*a) = a does not crash (issue #10240)
+    // uminus of a nonlinear product should not trigger NOT_IMPLEMENTED_YET
+    expr_ref x(m.mk_const("a", R), m);
+    expr_ref aa(a.mk_mul(x, x), m);
+    expr_ref neg_aa(a.mk_uminus(aa), m);
+    auto* n_neg_aa = get_node(g, a, neg_aa);
+    auto* n_x = get_node(g, a, x);
+    g.merge(n_neg_aa, n_x, nullptr);
+    g.propagate();
+    std::cout << "test4 passed\n";
+}
+
 void tst_euf_arith_plugin() {
     // enable_trace("plugin");
     test1();
     test2();
     test3();
+    test4();
 }