<div><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">Spear takes a different approach - it is bit-precise, handles all operators, but<br>currently doesn't handle arrays directly. However, the other mentioned
<br>thm provers<br>handle arrays by encoding them as UIFs + several axioms. As UIFs can be encoded<br>to SAT, I think that the theory of arrays could be as well. So, with a<br>bit of effort,<br>you should be able to use Spear for reasoning about arrays.
<br><br></blockquote></div>Thank you. I will try it.<br>But what I really mean is that array simulation is not an adequate solution to pointer problems. :-)<br>