From fef1596c813f0016a22f0febe335da52f61aea98 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 17 Jan 2024 15:11:06 -0800
Subject: [PATCH] pin expression passed to validate_eq

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_lra.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index b8c95e5c67f..b31867790b7 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -3499,7 +3499,8 @@ class theory_lra::imp {
         flet<bool> _svalid(s_validating, true);
         context nctx(m, ctx().get_fparams(), ctx().get_params());
         add_background(nctx);
-        nctx.assert_expr(m.mk_not(m.mk_eq(x->get_expr(), y->get_expr())));
+        expr_ref neq(m.mk_not(m.mk_eq(x->get_expr(), y->get_expr())), m);
+        nctx.assert_expr(neq);
         cancel_eh<reslimit> eh(m.limit());
         scoped_timer timer(1000, &eh);
         lbool r = nctx.check();