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

…alization
goblint · Sep 30, 2024 · abdc80a · abdc80a
1 parent da52931
commit abdc80a
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml
@@ -535,6 +535,10 @@ struct
           if M.tracing then M.trace "apron" "assert_constraint st: %a" D.pretty d;
           if M.tracing then M.trace "apron" "assert_constraint tcons1: %a" Tcons1.pretty tcons1;
           let r = meet_tcons ask d tcons1 e in
+          (* sv-benchmarks termination-restricted-15/IntPath needs stronger normalization for integers *)
+          (* let r = meet_tcons ask r tcons1 e in *) (* meeting twice works (polyhedra and octagon) *)
+          (* A.canonicalize Man.mgr r; *) (* this doesn't help *)
+          A.approximate Man.mgr r (-1); (* this also works, but does it approximate something away? (polyhedra only, octagon crashes) *)
           if M.tracing then M.trace "apron" "assert_constraint r: %a" D.pretty r;
           r
         | exception Convert.Unsupported_CilExp reason ->