Refactored the BMC induction algorithm so that the invariants formula is pushed onto the stack only once.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@11297 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
MathSAT 5.2.11


git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@11298 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Extract all code related to dynamic memory allocation into a single
class.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@11299 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Further unification of code for handling dynamic memory in one place.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@11300 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Cleanup

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@11301 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Remove outdated check for __content__ pseudo variables that no longer
exist.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@11302 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Always store canonicalized types in SSAMap.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@11303 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Fix bug in SSAMap merge where the type equality check was too strict.


git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@11304 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Fix missing detection of malloc function with too many parameters.


git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@11305 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Fixed error in expression simplifier.

The error was a result of having "strange" types as the result type of the expression(e.g. _Bool). For now resolved by just always assuming the expression is an integer.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@11306 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Implemented basic symbolic value formula handling with binary expressions.