From 99b71a9f9ed7478d3d651e5387433633a9150663 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 13 Feb 2020 16:28:36 -1000
Subject: [PATCH] fix #2975, parameter validation to avoid cases where domain
of sort is not fixed
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/qe/qsat.cpp | 7 +++++++
1 file changed, 7 insertions(+)
diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
index fb151d78e..650ad91bb 100644
--- a/src/qe/qsat.cpp
+++ b/src/qe/qsat.cpp
@@ -763,8 +763,15 @@ namespace qe {
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) {
for (app* v : vars) m_pred_abs.fmc()->hide(v);
+ for (app* v : vars) check_sort(m.get_sort(v));
}
void initialize_levels() {