Termination analysis: Insert only one increment statement, do not set…

… assume no overflow.

src/maingoblint.ml

@@ -164,8 +164,7 @@ let check_arguments () =
   if List.mem "termination" @@ get_string_list "ana.activated" then (
     if GobConfig.get_bool "incremental.load" || GobConfig.get_bool "incremental.save" then fail "termination analysis is not compatible with incremental analysis";
     set_list "ana.activated" (GobConfig.get_list "ana.activated" @ [`String ("threadflag")]);
-    set_string "sem.int.signed_overflow" "assume_none";
-    warn "termination analysis implicitly activates threadflag analysis and set sem.int.signed_overflow to assume_none"
+    warn "termination analysis implicitly activates threadflag analysis."
   );
   if not (get_bool "ana.sv-comp.enabled") && get_bool "witness.graphml.enabled" then fail "witness.graphml.enabled: cannot generate GraphML witness without SV-COMP mode (ana.sv-comp.enabled)"
 

src/util/terminationPreprocessing.ml

@@ -52,14 +52,8 @@ class loopCounterVisitor lc (fd : fundec) = object(self)
         let lval = Lval (Var v, NoOffset) in
         let init_stmt = mkStmtOneInstr @@ Set (var v, min_int_exp, loc, eloc) in
         let inc_stmt = mkStmtOneInstr @@ Set (var v, increment_expression lval, loc, eloc) in
-        let inc_stmt2 = mkStmtOneInstr @@ Set (var v, increment_expression lval, loc, eloc) in
         let exit_stmt = mkStmtOneInstr @@ Call (None, f_bounded, [lval], loc, locUnknown) in
-        (match b.bstmts with
-         | s :: ss ->   (*duplicate increment statement here to fix inconsistencies in nested loops*)
-           b.bstmts <- exit_stmt :: inc_stmt :: s :: inc_stmt2 :: ss;
-         | ss ->
-           b.bstmts <- exit_stmt :: inc_stmt :: ss;
-        );
+        b.bstmts <- exit_stmt :: inc_stmt :: b.bstmts;
         lc := VarToStmt.add (v: varinfo) (s: stmt) !lc;
         let nb = mkBlock [init_stmt; mkStmt s.skind] in
         s.skind <- Block nb;