Investigate a cvc4 model error
In VC test_map_multidim of map.mlw, the model of cvc4 stop after the first call to the prover. It returns:
(error "Array theory solver does not yet support write-chains connecting two different constant arrays")
It seems that only cvc4 1.7 returns such an error: cvc4 1.5 has a ok counterexample on this.