From 5ca53f37c00fa5aa7bbc713250092c3d9183ae3e Mon Sep 17 00:00:00 2001
From: Clemens Eisenhofer <56730610+CEisenhofer@users.noreply.github.com>
Date: Sat, 24 Sep 2022 18:54:14 +0200
Subject: [PATCH] Throw an exception if the variable in decide-callback is
 already assigned (#6362)

* Memory leak in .NET user-propagator
The user-propagator object has to be manually disposed (IDisposable), otherwise it stays in memory forever, as it cannot be garbage collected automatically

* Throw an exception if variable passed to decide is already assigned instead of running in an assertion violation
---
 src/smt/theory_user_propagator.cpp | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp
index b8efea851..7bbf9d925 100644
--- a/src/smt/theory_user_propagator.cpp
+++ b/src/smt/theory_user_propagator.cpp
@@ -249,7 +249,11 @@ void theory_user_propagator::decide(bool_var& var, bool& is_pos) {
 
     // get unassigned variable from enode
     var = enode_to_bool(new_enode, new_bit);
-
+    
+    if (var == null_bool_var)
+        // selected variable is already assigned
+        throw default_exception("expression in \"decide\" is already assigned");
+    
     // in case the callback did not decide on a truth value -> let Z3 decide
     is_pos = ctx.guess(var, phase);
 }