SMT for state-based formal methods: the ASM case study