From af270da785e1b15614951678e963a73c3e0d544d Mon Sep 17 00:00:00 2001
From: Can Cebeci <can.cebeci@epfl.ch>
Date: Thu, 6 Feb 2025 01:14:55 +0100
Subject: [PATCH] Fix complete_partial_func for finite domains (#7547)
---
src/smt/proto_model/proto_model.cpp | 10 ++++------
1 file changed, 4 insertions(+), 6 deletions(-)
diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp
index 85100cb09..90214a4be 100644
--- a/src/smt/proto_model/proto_model.cpp
+++ b/src/smt/proto_model/proto_model.cpp
@@ -345,14 +345,12 @@ void proto_model::compress() {
void proto_model::complete_partial_func(func_decl * f, bool use_fresh) {
func_interp * fi = get_func_interp(f);
if (fi && fi->is_partial()) {
- expr * else_value;
- if (use_fresh) {
+ expr * else_value = nullptr;
+ if (use_fresh)
else_value = get_fresh_value(f->get_range());
- }
- else {
+ if (!else_value)
else_value = fi->get_max_occ_result();
- }
- if (else_value == nullptr)
+ if (!else_value)
else_value = get_some_value(f->get_range());
fi->set_else(else_value);
}