We already provide a warning for unguarded pre expressions as part of our static analysis. For a solver like yices we should be able to detect when a counterexample relies on values before the initial time step. We should think about reporting this information to the user. (Suggested by Dan DaCosta)
We already provide a warning for unguarded pre expressions as part of our static analysis. For a solver like yices we should be able to detect when a counterexample relies on values before the initial time step. We should think about reporting this information to the user. (Suggested by Dan DaCosta)