Skip to content

Make AssumptionCollectorAlgorithm output C-like assumptions

Thomas Lemberger requested to merge assumption-automaton-fix into trunk

Currently, assumptions collected for conditional model checking are exported to condition automata as SMTlib formulae. But the condition automaton actually requires C-like expressions.

This MR changes the export of assumptions by parsing the boolean formulas stored in the AssumptionStorageState into C.

There's some unrelated formatting in the MR changes; the relevant changes start here: !71 (diffs)

Edited by Thomas Lemberger

Merge request reports