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