euf_arith_plugin: implement uminus instead of NOT_IMPLEMENTED_YET (#10243)

`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

@@ -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);
         }
 
     }

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();
 }