From a6b12bb33ce4936002f0d30ef98941d92795599c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 10 Feb 2025 14:38:59 -0800
Subject: [PATCH] call make-feasible after values are initialized

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

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 7d320ecb1..9b9f284fb 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -2930,8 +2930,7 @@ namespace smt {
     void context::set_sls_value(expr* var, expr* value) {
         expr_ref _var(var, m);
         expr_ref _valueu(value, m);
-#if 0
-// temporary disabled
+#if 1
         if (!e_internalized(var))
             return;
         enode* n = get_enode(var);
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 11738e266..87dc6af0b 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -993,6 +993,7 @@ public:
             return;
         }
         lp().move_lpvar_to_value(get_lpvar(var), r);
+        make_feasible();
     }
 
     void new_eq_eh(theory_var v1, theory_var v2) {