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

fix #2975, parameter validation to avoid cases where domain of sort is not fixed

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-13 16:28:36 -10:00
parent b96e203aea
commit 99b71a9f9e
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/qe/qsat.cpp
View file

@ -763,8 +763,15 @@ namespace qe {
TRACE("qe", tout << fml << "\n";); TRACE("qe", tout << fml << "\n";);
} }
void check_sort(sort* s) {
if (m.is_uninterp(s)) {
throw default_exception("qsat does not apply to uninterpreted sorts");
}
}
void filter_vars(app_ref_vector const& vars) { void filter_vars(app_ref_vector const& vars) {
for (app* v : vars) m_pred_abs.fmc()->hide(v); for (app* v : vars) m_pred_abs.fmc()->hide(v);
for (app* v : vars) check_sort(m.get_sort(v));
} }
void initialize_levels() { void initialize_levels() {