Towards SV-COMP
Issues that need to be solved in order to be able to run SV-COMP benchmarks.
$ divine verify --symbolic test/abstract/2.svc-a.c
loading bitcode … LART … setting up pass: abstraction, options = sym
divine: /home/xstill/DIVINE/divine4/llvm/include/llvm/Support/Casting.h:237: typename cast_retty<X, Y *>::ret_type llvm::cast(Y *) [X = llvm::CallInst, Y = llvm::User]: Assertion `isa<X>(Val) && "cast<Ty>() argument of incompatible type!"' failed.
Aborted
$ divine verify --symbolic test/abstract/2.svc-b.c
loading bitcode … LART … setting up pass: abstraction, options = sym
E: Invalid bitcode: Wrong types for attribute: signext zeroext
%"union.sym::Formula.2"* ()* @__VERIFIER_nondet_short.1255.1256
Aborted