analyzer icon indicating copy to clipboard operation
analyzer copied to clipboard

Try to fix sv-benchmarks termination-restricted-15/IntPath Apron normalization

Open sim642 opened this issue 1 year ago • 0 comments

As identified in https://github.com/goblint/analyzer/issues/1576#issuecomment-2378939924, this SV-COMP task causes a weird both branches dead situation which actually is sound. With both octagon and polyhedra, there are constraints like 2x=1 where x is an integer. Neither domain seems to immediately reduce this to bottom to make it dead. Only later when re-asserting some (even the same) constraint, it's somehow checked again and does become dead, but in both branches.

Here are a few attempts to try to make this come out early, but I don't think none are particularly nice. It's hard to tell where Apron actually applies some integer reduction. It seems to be a separate thing from other kinds of normalization/closure/canonicalization that Apron has and does.

sim642 avatar Sep 30 '24 08:09 sim642