You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: src/solver/td3.ml
+10-13Lines changed: 10 additions & 13 deletions
Original file line number
Diff line number
Diff line change
@@ -350,18 +350,15 @@ module Base =
350
350
351
351
let wpd =(* d after widen/narrow (if wp) *)
352
352
ifnot wp then eqd
353
-
else (
354
-
if term then
355
-
match phase with
356
-
|Widen -> S.Dom.widen old (S.Dom.join old eqd)
357
-
|NarrowwhenGobConfig.get_bool "exp.no-narrow" -> old (* no narrow *)
358
-
|Narrow ->
359
-
(* assert S.Dom.(leq eqd old || not (leq old eqd)); (* https://github.com/goblint/analyzer/pull/490#discussion_r875554284 *)*)
360
-
S.Dom.narrow old eqd
361
-
else (
362
-
box old eqd
363
-
)
364
-
)
353
+
elseif term then
354
+
match phase with
355
+
|Widen -> S.Dom.widen old (S.Dom.join old eqd)
356
+
|NarrowwhenGobConfig.get_bool "exp.no-narrow" -> old (* no narrow *)
357
+
|Narrow ->
358
+
(* assert S.Dom.(leq eqd old || not (leq old eqd)); (* https://github.com/goblint/analyzer/pull/490#discussion_r875554284 *)*)
359
+
S.Dom.narrow old eqd
360
+
else
361
+
box old eqd
365
362
in
366
363
if tracing then trace "sol""Var: %a (wp: %b)\nOld value: %a\nEqd: %a\nNew value: %a"S.Var.pretty_trace x wp S.Dom.pretty old S.Dom.pretty eqd S.Dom.pretty wpd;
367
364
if cache then (
@@ -370,7 +367,7 @@ module Base =
370
367
);
371
368
ifnot (Timing.wrap "S.Dom.equal" (fun() -> S.Dom.equal old wpd) ()) then ( (* value changed *)
372
369
if tracing then trace "sol""Changed";
373
-
(* if tracing && not (S.Dom.is_bot old) && wp then trace "solchange" "%a (wpx: %s): %a -> %a" S.Var.pretty_trace x (format_wpoint x) S.Dom.pretty old S.Dom.pretty wpd; *)
370
+
(* if tracing && not (S.Dom.is_bot old) && wp then trace "solchange" "%a (wpx: %a): %a -> %a" S.Var.pretty_trace x pretty_wpoint x S.Dom.pretty old S.Dom.pretty wpd; *)
374
371
if tracing &¬ (S.Dom.is_bot old) && wp then trace "solchange""%a (wpx: %a): %a"S.Var.pretty_trace x pretty_wpoint x S.Dom.pretty_diff (wpd, old);
0 commit comments