mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 11:12:28 +00:00
Code Activity

fixup

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-10-16 13:30:02 +02:00
parent 26d37c7b30
commit ed369dee08
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/model/finite_set_value_factory.cpp
View file

@ -50,6 +50,7 @@ expr * finite_set_value_factory::get_fresh_value(sort * s) {
auto& [set_e, values_e] = get_value_set(elem_sort);
unsigned next_index = values.size();
// Course Task of 10-16-25:
// For finite domains, we may not be able to generate fresh values
// if all values have been exhausted
// create sets based on next_index