Karlheinz Friedberger

@tautschnig : This is a reminder. Are there any news on this topic?

Surprisingly most of the provided witnesses are quite short. CPAchecker can also be executed to directly verify those files: `scripts/cpa.sh -smg -spec test/programs/benchmarks/properties/valid-memsafety.prp -64 SOURCEFILE` As CPAchecker might in theory...

No, that is not sufficient, but a good heuristic. Some files might include others or depend on them. Sometimes, we change global scripts, options like machinemodel, or the compiler. Currently,...

CPAchecker cannot handle SIN and COS and simply ignores these functioncalls (when used as validator). Thus I would not trust CPAchecker as a validator for this task. :-) @animeshbchowdhury Your...

That would be a good idea. At least the property `valid-deref` might be violated.

The commit e76bcd9 is quite old (over 4 years). At that time I worked with Ubuntu 12.04 or 14.04 or Arch Linux (rolling release, no version number), all of them...

We have now an initial working version of CVC5 1.0.1 available via Ivy. We can now take a look at the API and bugs related to its usage.

The following bugs in the JavaSMT-bindings for CVC5 are currently known and will be analyzed in the next days: - Formulas from model evaluation are cleaned up when closing the...

Update for the last comment: - Formulas from model need to be converted from one solver instance to another one. This is not easily doable from JavaSMT-ide, because we would...

The current status of this branch is that most solver functionality should work as expected and there are some minor issues, mostl performance-related. I suggest to merge this PR and...