From 18b4c7e99b690db43f1ae6bdab75bdf6e5b07e43 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 6 Apr 2020 17:09:23 -0700
Subject: [PATCH] fix #3796

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/rel/dl_finite_product_relation.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/muz/rel/dl_finite_product_relation.cpp b/src/muz/rel/dl_finite_product_relation.cpp
index 7b6a46796..d4611e4c2 100644
--- a/src/muz/rel/dl_finite_product_relation.cpp
+++ b/src/muz/rel/dl_finite_product_relation.cpp
@@ -1417,6 +1417,8 @@ namespace datalog {
                 relation_base * new_rel = old_rel.clone();
 
                 scoped_ptr<relation_mutator_fn> filter = rmgr.mk_filter_interpreted_fn(*new_rel, to_app(inner_cond));
+                if (!filter)
+                    throw default_exception("rules do not belong to supported finite domain fragment");
                 (*filter)(*new_rel);
 
                 if(new_rel->empty()) {