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
Fix assertion in test (found by FindBugs)

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14560 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Test commit for testing commit hooks -- please ignore.


git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14561 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Delete directory that commit hook should have prevented.


git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14562 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
rename ValueAnalysisGlobalRefiner to ValueAnalysisRefiner; the ValueAnalysisRefiner works with both, global refinement and single path refinements, as the latter is only a special case of the former

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14563 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
set default to BOTTOM (instead of TOP) for option cpa.value.refinement.restart, this resembles more the way it worked before (i.e., lazy-abstraction, where lower parts of ARG are refined, instead restarting at root node [c.f. cpa.value.refinement.restart=TOP])

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14564 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Update Z3 to a new version.

60aad7a6623182eddc63d949cee4fde98922c65d + cherry-picked
091ef3dbec53d1ff7065bc9b0bf22a77c1efdccc

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14566 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Replace epsilons returned by Z3 opt-branch

by actual values.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14567 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Removes unnecessary code from policy iteration.

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

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

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14570 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Add a fourth parameter to PrecisionAdjustment operator
that gives access to the abstract states of other CPAs.
This can be used for example to access the current location
from within any CPA.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14571 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Use the newly added fourth parameter for precision adjustment in ValueAnalysisPrecisionAdjustment instead of saving the last location in the transfer relation (this was imprecise in some cases)

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14572 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
changed toDotLabel() of SignState and ReachingDefState

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14573 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
refactored value static refiner; removed its reference from ValueCPA and added it to DelegatingRefiner along the way

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