From 604971d651017e90cd66fd3fc3a82945341269f0 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 9 Jan 2015 22:23:55 +0100 Subject: [PATCH] postproc: use scc_filter_states on SBA * src/tgbaalgos/postproc.cc: Here. Otherwise, reading a neverclaim with autfilt would loose the SBA property and degeneralize again. --- src/tgbaalgos/postproc.cc | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/tgbaalgos/postproc.cc b/src/tgbaalgos/postproc.cc index 1adbaff50..bf7f919f9 100644 --- a/src/tgbaalgos/postproc.cc +++ b/src/tgbaalgos/postproc.cc @@ -149,7 +149,12 @@ namespace spot // ignored. a = scc_filter_states(a); else if (scc_filter_ > 0) - a = scc_filter(a, scc_filter_ > 1); + { + if (type_ == BA && a->is_sba()) + a = scc_filter_states(a); + else + a = scc_filter(a, scc_filter_ > 1); + } if (type_ == Monitor) {