Skip to content
  • Alexandre Duret-Lutz's avatar
    fix a memory leak in basic LTL simplifications · a9fc213a
    Alexandre Duret-Lutz authored
    When something like XFa & FXa is reduced, the subformulae XFa and FXa
    are both rewritten separately to XFa, and then the vector of arguments
    of the And operators, [XFa,XFa], is passed through a specialized loop
    that searches of the form X(...) that can potentially be simplified with
    some other terms.  This loop converts the vector [XFa,XFa] into the set
    {XFa,XFa}={XFa} and forgot to deal with the case where the insertion
    would actually not add an existing subformula.
    
    * src/ltlvisit/simplify.cc: Fix the code for Or, and And.
    * src/ltltest/reduc0.test: New file, to test it.
    * src/ltltest/Makefile.am (TESTS): Add it.
    * src/ltltest/reduccmp.test: Add an extra test that does not
    trigger the bug (because reduccmp.test uses more than basic
    optimizations, and the implication-based simplifications are
    already able to detect that XFa and FXa are equivalent).
    a9fc213a