Some utilities for CTypes.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14540 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Pass Constraint object down to CtoFormulaConverter.makeSimpleCast()

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14541 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
several bugfixes for LiveVariablesTransferrelation

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

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

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14544 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Refactoring of the LiveVariablesTransferrelation

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14545 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Remove unused option

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14546 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Installed a custom error handler for Z3.

Upgraded Z3 version to 60aad7a6623182eddc63d949cee4fde98922c65d,
latest version before the interpolation interface was changed.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14547 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Array Theory: Introduced an ArrayFormula type.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14548 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Improve PathFormulaTest:
asserts with better messages,
more precise checks for expected exceptions

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14549 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Remove redundant tests.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14550 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Add forgotten line to test.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14551 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Policy Iteration: path focusing implementation.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14552 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Switched to non-deprecated function for Z3 error

reporting.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14553 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Array Theory: Type for array index and its elements.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14554 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Support for compiling the Z3 wrapper on Windows.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14555 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Better support for Windows. Compiling the Z3 wrapper on Windows requires a cross-compiler.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14556 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
refactoring of value refinement

the DelegatingRefiner now also delegates to a refiner for the value domain, instead of performing value refinements itself

with this change, refinement for the BDD domain by means of the ValueRefiner is for now no longer supported

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14557 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Add more documentation with hints for writing tests.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14558 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Fix exceptions that happen when a timeout
occurs during a SAT check in MathSAT.

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