Version submitted to TACAS'20