Figure out how to properly do the invariant backtranslation in transformation to single TS

usi-verification-and-security / golem

Solver for Constrained Horn Clauses

MIT License

34 stars 7 forks source link

Figure out how to properly do the invariant backtranslation in transformation to single TS #45

Closed blishko closed 5 months ago

blishko commented 11 months ago

For example chc22/LIA-Lin/chc-LIA-Lin_082.smt2 for engine imc currently runs into alien variables in vertex invariant and is therefore unable to proceed with the backtranslation.