alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

synthesis: Fix for implication decomposition

Browse source 
* spot/twaalgos/synthesis.cc: here
This commit is contained in:
Florian Renkin 2022-09-03 14:04:41 +02:00
parent 3cd43f618c
commit 27816ea438
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
spot/twaalgos/synthesis.cc
View file

@ -1737,7 +1737,7 @@ namespace // anonymous for subsformula
std::vector<formula> children;
for (auto fi : f)
children.push_back(
extract_and(fi, outs, can_extract_impl, form2props));
extract_and(fi, outs, false, form2props));
return formula::And(children);
}
if (f.is(op::Not))