modified benchmark files for partial certificate evaluation

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13191 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
added benchmark files for interleaved certificate reading and checking

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13192 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Integrated the new graphml error witness parser created by Andreas.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13194 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Implemented the unsound approach of adding pre-loop information to the induction hypothesis of k-induction. This approach was introduced by the SV-COMP 2013 competition contribution of ESBMC 1.20.

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

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13196 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Adding API for the optimization queries using the Z3 solver.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13197 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Adding features to the [rationals] library.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13198 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Z3 optimization API - adding the getter to the FormulaManagerFactory

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13199 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Max-policy iteration: work in progress.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13200 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Updates to the "rationals" library

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13201 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Logging for the optimization solver.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13202 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Refactoring out CPA testing

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13203 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Policy Iteration: work-in-progress

There is an automated test.
Value determination produces formulas.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13204 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Policy Iteration: work-in-progress

Value determination starts to terminate.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13205 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Decrease the reference counter for Z3 expressions in the finalizer

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13206 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Provides interface for substituting expressions inside Formulas (currently only implemented in Z3)

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13207 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Changed [SSAMap::withDefault] method to static for greater usability

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13208 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Policy Iteration: work-in-progress

Value determination formulas seem to be correct.

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

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@13210 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Max-Policy iteration works!

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