From abdc80a93a31e5695291b1711f9b7cd3b7ab36a8 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 30 Sep 2024 11:19:18 +0300 Subject: [PATCH] Try to fix sv-benchmarks termination-restricted-15/IntPath Apron normalization --- src/cdomains/apron/apronDomain.apron.ml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml index 03ac3ed3f0..0d331862c8 100644 --- 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 ->