Section 5, step 6 of paper is incorrect.

[roberthsheng]

We finally add one of the two conjuncts (a) ¬φ_t′ or (b) φ_t′ alternatively, where t′ = t − duration(φ), to the resultant constraint system and check both variants for their satisfiability using an SMT-LA solver. Depending on the results of the two satisfiability checks, we report inconclusive if both systems are found to be satisfiable, ⊤ if the system (a) containing ¬φ_t′ is unsatisfiable, ⊥ if the system (b) containing φ_t′ is unsatisfiable.

[roberthsheng]

When True, the system should always be satisfiable, but ¬φ should be set to False and φ should be set to True.

[roberthsheng]

Wait no