From 780ad7cc179aa38648a2aca7c6a1d8a99ff42763 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 25 Apr 2013 09:30:51 -0700
Subject: [PATCH] fix seg-fault caused by neglecting to inherit output
predicate in slice
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/muz_qe/dl_mk_slice.cpp | 3 +++
1 file changed, 3 insertions(+)
diff --git a/src/muz_qe/dl_mk_slice.cpp b/src/muz_qe/dl_mk_slice.cpp
index 21c3486b3..89804447b 100644
--- a/src/muz_qe/dl_mk_slice.cpp
+++ b/src/muz_qe/dl_mk_slice.cpp
@@ -725,6 +725,9 @@ namespace datalog {
m_mc->add_predicate(p, f);
}
}
+ else if (src.is_output_predicate(p)) {
+ dst.set_output_predicate(p);
+ }
}
}