mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-06 14:26:03 +00:00
Code Activity

Add SASSERT for finite set check in factory

Browse source 
Added assertion to check if the sort is a finite set.
This commit is contained in:
Nikolaj Bjorner 2025-10-16 12:48:50 +02:00 • committed by GitHub
parent 75749dc441
commit 295d02397b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/model/finite_set_value_factory.cpp
View file

@ -12,7 +12,6 @@ Abstract:
--*/ --*/
#include "model/finite_set_value_factory.h" #include "model/finite_set_value_factory.h"
#include "model/model_core.h" #include "model/model_core.h"
#include "ast/array_decl_plugin.h"
finite_set_value_factory::finite_set_value_factory(ast_manager & m, family_id fid, model_core & md): finite_set_value_factory::finite_set_value_factory(ast_manager & m, family_id fid, model_core & md):
struct_factory(m, fid, md), struct_factory(m, fid, md),
@ -22,6 +21,7 @@ finite_set_value_factory::finite_set_value_factory(ast_manager & m, family_id fi
expr * finite_set_value_factory::get_some_value(sort * s) { expr * finite_set_value_factory::get_some_value(sort * s) {
// Check if we already have a value for this sort // Check if we already have a value for this sort
value_set * set = nullptr; value_set * set = nullptr;
SASSERT(u.is_finite_set(s));
if (m_sort2value_set.find(s, set) && !set->empty()) if (m_sort2value_set.find(s, set) && !set->empty())
return *(set->begin()); return *(set->begin());