(************************************************************
 *                      IMITATOR MODEL
 *
 * Toy benchmark for which the result is easy for hand computation but IMITATOR cannot find it because the accumulated constraints grow forever
 *
 * Description     : Toy benchmark for which the result is easy for hand computation but IMITATOR cannot find it because the accumulated constraints grow forever
 * Correctness     : Reachability
 * Source          : Own work
 * Author          : Étienne André
 * Modeling        : Étienne André
 * Input by        : Étienne André
 * License         : Creative Commons Attribution-ShareAlike 4.0 International (CC BY-SA 4.0)
 *
 * Created         : 2020/09/24
 * Last modified   : 2021/01/21
 *
 * Computation     : Unsolvable
 *
 * IMITATOR version: 3.0
 ************************************************************)

property := #synth EF(loc[pta] = lGoal);