mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

Throw an exception if the variable in decide-callback is already assigned (#6362)

Browse source 
* 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
This commit is contained in:
Clemens Eisenhofer 2022-09-24 18:54:14 +02:00 committed by GitHub
parent 3dfff3d7a1
commit 5ca53f37c0
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/smt/theory_user_propagator.cpp
View file

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