Age | Commit message (Collapse) | Author | |
---|---|---|---|
2017-10-16 | Fix for issue 1247 (#1257) | Clark Barrett | |
* Fix for bug 1247: in incremental mode, there was a corner case where a skolem variable introduced during ITE removal became a solved-for variable (part of the substitution map). But then if the same skolem was introduced again as part of a subsequent ITE removal pass, the substitution was not properly applied and an incorrect result was obtained. The handling of substitutions in incremental mode is quite kludgey - I opened an issue to revisit this. * fixing regression |