Added a default name for witness automata.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14013 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Add the function msat_make_int_modular_congruence to the native api of
our MathSAT wrapper (will be available when MathSAT is recompiled).

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14014 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Fixed a bug where the initial loop stack state for locations within loops was wrongly initialized with 0 when it should have been 1.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14015 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Fixed a bug where the token number 0 was exported to the witness when a dummy file location appeared on an edge of the error path.

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

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14017 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Refactor: Use constant for reoccurring String with special meaning, correct comment.



git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14018 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Fixing NPE for multiple successive component aware precision adjustments on the same value analysis state.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14019 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
added the possibility to disable tracking addressed variables (&a) to the VariableTrackingPrecision

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14020 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Updated configuration option documentation for the option added in r14020

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14021 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Add more comments to LoopStructure and Loop classes.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14022 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Cut correct amount of characters in JArrayInitializer.toString()


git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14023 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Use ImmutableList in JArrayCreationExpression to avoid unintended changes to expression.



git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14024 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Fixed a bug where the single loop transformation produced erroneous results when using transformation strategies other than MULTIPLE_PATHS.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14025 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Remove unused fields of RefinementFailedException,
add possibility to pass a Throwable

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14027 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Catch some exceptions which indicate known MathSAT problems
such that CPAchecker can return UNKNOWN
instead of printing an exception stack trace.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14028 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
FunctionEntryNode needs to be an abstract class
because it has a method that cannot be implemented
(and "return null" is not a valid replacement).

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14029 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Fix exception in ErrorPathShrinker for FunctionCallEdges with varargs.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14030 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
Fix bugfix for #178:
When looking at function types, we need to get the canonical type
to resolve typedefs, but we may not resolve the parameter types,
because otherwise elaborated types in the parameters get resolved
to struct types, and this produces illegal C code.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14031 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
SMGCPA: Prepare for symbolic abstraction.

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/trunk@14032 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c
SMGCPA: Not every pointer is written into the smg when evaluated (e.g
&a->x). Adjusted binary evaluation.

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