Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fixpoints not being reached #153

Closed
6 tasks done
michael-schwarz opened this issue Dec 2, 2020 · 15 comments
Closed
6 tasks done

Fixpoints not being reached #153

michael-schwarz opened this issue Dec 2, 2020 · 15 comments
Labels
bug sv-comp SV-COMP (analyses, results), witnesses
Milestone
SV-COMP 2023

Comments

@michael-schwarz
Copy link
Member

michael-schwarz commented Dec 2, 2020 •
edited by sim642
Loading

SV-Comp '21 revealed a few example programs where we do not reach the fixpoint:

  • c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v%2Bcfa-reducer.yml
  • c/seq-mthreaded-reduced/pals_opt-floodmax.5.1.ufo.BOUNDED-10.pals.c.v%2Bnlh-reducer.yml
  • c/seq-mthreaded-reduced/pals_opt-floodmax.5.2.ufo.UNBOUNDED.pals.c.v%2Bcfa-reducer.yml
  • c/seq-mthreaded-reduced/pals_opt-floodmax.5.3.ufo.BOUNDED-10.pals.c.v%2Bnlh-reducer.yml
  • c/seq-mthreaded-reduced/pals_opt-floodmax.5.4.ufo.BOUNDED-10.pals.c.v%2Bnlh-reducer.yml
  • c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c (surfaced after merging 0f9f068)
@michael-schwarz
Copy link
Member Author

michael-schwarz commented Dec 3, 2020 •
edited
Loading

It seems like this is an issue with the thread analysis (#130), if I disable it, we reach the fixpoint.
For the first example at least, var_eq contains an additional equality between {0, main__i2} in what the solver computed, that is not there for the RHS, but he value domain still knows that main__i2 is [0,0].

@sim642
Copy link
Member

sim642 commented Dec 3, 2020

Could it be that this is also the fault of WitnessConstraints.PathSensitive3? Or does this also happen outside of SV-COMP mode?

Because it seems weird that the difference is in var_eq but somehow thread is at fault? Also #130 and #137 didn't really change the local domain of thread, so I'm not sure how it's related. But I also haven't looked into this yet.

@michael-schwarz
Copy link
Member Author

Yes, could be. It only happens with ana.sv-comp.enabled on.

@sim642
Copy link
Member

sim642 commented Dec 7, 2020

This is weird. I just locally tried all of them under the svcomp21 tag and they all give unknown result instead of ERROR (verify). So I can't even reproduce this issue.

The log for those from SV-COMP preruns also has a weird like:

Difference: Set (Set (Cil expressions)): These are fine!.

That seems to indicate there is no problem.

@michael-schwarz
Copy link
Member Author

I can reproduce it, also with the latest commits on master:

 ./goblint --conf conf/svcomp21.json --sets ana.specification ../../sv-comp/sv-benchmarks/c/properties/unreach-call.prp --html  ../../sv-comp/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c
SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
Fixpoint not reached at node 501 "(int )assert__arg == 0" on pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:722 (../../sv-comp/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:722)
 Solver computed:
 (mapping {
    [Topped Set (variables):{}, lifted regmap:mapping {
                                                },
     Reversed (Topped Set (Cil expressions)):{},
     Topped Set (Set (Cil expressions)):{{0, main__i2}, {__tmp_1, assert__arg, main__c1}, {init__r122, init__tmp}, {init__r123, init__tmp___11}, {init__r132, init__tmp___0}, {init__r133, init__tmp___12}, {init__r142, init__tmp___1}, {init__r143, init__tmp___13}, {init__r212, init__tmp___2}, {init__r213, init__tmp___14}, {init__r232, init__tmp___3}, {init__r233, init__tmp___15}, {init__r242, init__tmp___4}, {init__r243, init__tmp___16}, {init__r312, init__tmp___5}, {init__r313, init__tmp___17}, {init__r322, init__tmp___6}, {init__r323, init__tmp___18}, {init__r342, init__tmp___7}, {init__r343, init__tmp___19}, {init__r412, init__tmp___8}, {init__r413, init__tmp___20}, {init__r422, init__tmp___9}, {init__r423, init__tmp___21}, {init__r432, init__tmp___10}, {init__r433, init__tmp___22}},
     Unit:(), Topped Set (variables):{},
     Reversed (Topped Set (Normal Lvals * booleans)):{}, MT mode:Singlethreaded,
     Thread:main,
     value domain * array partitioning deps:(mapping {
                                               Global {
                                                 __return_main -> (0,[0,0])
                                                 nomsg -> (-1,[-1,-1])
                                                 p12 -> (0,[0,0])
                                                 p12_old -> (Unknown int([-7,7]),[-1,127])
                                                 p12_new -> (-1,[-1,-1])
                                                 ep12 -> (Unknown int([0,1]),[0,1])
                                                 p13 -> (0,[0,0])
                                                 p13_old -> (Unknown int([-7,7]),[-1,127])
                                                 p13_new -> (-1,[-1,-1])
                                                 ep13 -> (Unknown int([0,1]),[0,1])
                                                 p14 -> (0,[0,0])
                                                 p14_old -> (Unknown int([-7,7]),[-1,127])
                                                 p14_new -> (-1,[-1,-1])
                                                 ep14 -> (Unknown int([0,1]),[0,1])
                                                 p21 -> (0,[0,0])
                                                 p21_old -> (Unknown int([-7,7]),[-1,127])
                                                 p21_new -> (-1,[-1,-1])
                                                 ep21 -> (Unknown int([0,1]),[0,1])
                                                 p23 -> (0,[0,0])
                                                 p23_old -> (Unknown int([-7,7]),[-1,127])
                                                 p23_new -> (-1,[-1,-1])
                                                 ep23 -> (Unknown int([0,1]),[0,1])
                                                 p24 -> (0,[0,0])
                                                 p24_old -> (Unknown int([-7,7]),[-1,127])
                                                 p24_new -> (-1,[-1,-1])
                                                 ep24 -> (Unknown int([0,1]),[0,1])
                                                 p31 -> (0,[0,0])
                                                 p31_old -> (Unknown int([-7,7]),[-1,127])
                                                 p31_new -> (-1,[-1,-1])
                                                 ep31 -> (Unknown int([0,1]),[0,1])
                                                 p32 -> (0,[0,0])
                                                 p32_old -> (Unknown int([-7,7]),[-1,127])
                                                 p32_new -> (-1,[-1,-1])
                                                 ep32 -> (Unknown int([0,1]),[0,1])
                                                 p34 -> (0,[0,0])
                                                 p34_old -> (Unknown int([-7,7]),[-1,127])
                                                 p34_new -> (-1,[-1,-1])
                                                 ep34 -> (Unknown int([0,1]),[0,1])
                                                 p41 -> (0,[0,0])
                                                 p41_old -> (Unknown int([-7,7]),[-1,127])
                                                 p41_new -> (-1,[-1,-1])
                                                 ep41 -> (Unknown int([0,1]),[0,1])
                                                 p42 -> (0,[0,0])
                                                 p42_old -> (Unknown int([-7,7]),[-1,127])
                                                 p42_new -> (-1,[-1,-1])
                                                 ep42 -> (Unknown int([0,1]),[0,1])
                                                 p43 -> (0,[0,0])
                                                 p43_old -> (Unknown int([-7,7]),[-1,127])
                                                 p43_new -> (-1,[-1,-1])
                                                 ep43 -> (Unknown int([0,1]),[0,1])
                                                 id1 -> (Unknown int([-7,7]),[0,127])
                                                 r1 -> (Unknown int([0,8]),[0,255])
                                                 st1 -> (Unknown int([0,7]),[0,127])
                                                 nl1 -> (Unknown int([0,7]),[0,127])
                                                 m1 -> (Unknown int([-7,7]),[-128,127])
                                                 max1 -> (Unknown int([-7,7]),[0,127])
                                                 mode1 -> (Unknown int([0,7]),[0,1])
                                                 newmax1 -> (Unknown int([0,1]),[0,1])
                                                 id2 -> (Unknown int([-7,7]),[0,127])
                                                 r2 -> (Unknown int([0,8]),[0,255])
                                                 st2 -> (Unknown int([0,7]),[0,127])
                                                 nl2 -> (Unknown int([0,7]),[0,127])
                                                 m2 -> (Unknown int([-7,7]),[-128,127])
                                                 max2 -> (Unknown int([-7,7]),[0,127])
                                                 mode2 -> (Unknown int([0,7]),[0,1])
                                                 newmax2 -> (Unknown int([0,1]),[0,1])
                                                 id3 -> (Unknown int([-7,7]),[0,127])
                                                 r3 -> (Unknown int([0,8]),[0,255])
                                                 st3 -> (Unknown int([0,7]),[0,127])
                                                 nl3 -> (Unknown int([0,7]),[0,127])
                                                 m3 -> (Unknown int([-7,7]),[-128,127])
                                                 max3 -> (Unknown int([-7,7]),[0,127])
                                                 mode3 -> (Unknown int([0,7]),[0,1])
                                                 newmax3 -> (Unknown int([0,1]),[0,1])
                                                 id4 -> (Unknown int([-7,7]),[0,127])
                                                 r4 -> (Unknown int([0,8]),[0,255])
                                                 st4 -> (Unknown int([0,7]),[0,127])
                                                 nl4 -> (Unknown int([0,7]),[0,127])
                                                 m4 -> (Unknown int([-7,7]),[-128,127])
                                                 max4 -> (Unknown int([-7,7]),[0,127])
                                                 mode4 -> (Unknown int([0,7]),[0,1])
                                                 newmax4 -> (Unknown int([0,1]),[0,1])
                                                 nodes -> 
                                                   (Array: Array (no part.): {&node1, &node2, &node3, &node4}, (Error int,bottom))
                                                 __return_3435 -> (1,[1,1])
                                                 __return_3681 -> (Unknown int([0,7]),[0,1])
                                               }
                                               Local {
                                                 main__c1 -> (Unknown int([0,7]),[0,1])
                                                 main__i2 -> (0,[0,0])
                                                 init__r121 -> (Unknown int([0,1]),[0,1])
                                                 init__r131 -> (Unknown int([0,1]),[0,1])
                                                 init__r141 -> (Unknown int([0,1]),[0,1])
                                                 init__r211 -> (Unknown int([0,1]),[0,1])
                                                 init__r231 -> (Unknown int([0,1]),[0,1])
                                                 init__r241 -> (Unknown int([0,1]),[0,1])
                                                 init__r311 -> (Unknown int([0,1]),[0,1])
                                                 init__r321 -> (Unknown int([0,1]),[0,1])
                                                 init__r341 -> (Unknown int([0,1]),[0,1])
                                                 init__r411 -> (Unknown int([0,1]),[0,1])
                                                 init__r421 -> (Unknown int([0,1]),[0,1])
                                                 init__r431 -> (Unknown int([0,1]),[0,1])
                                                 init__r122 -> (Unknown int([0,1]),[0,1])
                                                 init__tmp -> (Unknown int([0,7]),[0,1])
                                                 init__r132 -> (Unknown int([0,1]),[0,1])
                                                 init__tmp___0 -> (Unknown int([0,7]),[0,1])
                                                 init__r142 -> (Unknown int([0,1]),[0,1])
                                                 init__tmp___1 -> (Unknown int([0,7]),[0,1])
                                                 init__r212 -> (Unknown int([0,1]),[0,1])
                                                 init__tmp___2 -> (Unknown int([0,7]),[0,1])
                                                 init__r232 -> (Unknown int([0,1]),[0,1])
                                                 init__tmp___3 -> (Unknown int([0,7]),[0,1])
                                                 init__r242 -> (Unknown int([0,1]),[0,1])
                                                 init__tmp___4 -> (Unknown int([0,7]),[0,1])
                                                 init__r312 -> (Unknown int([0,1]),[0,1])
                                                 init__tmp___5 -> (Unknown int([0,7]),[0,1])
                                                 init__r322 -> (Unknown int([0,1]),[0,1])
                                                 init__tmp___6 -> (Unknown int([0,7]),[0,1])
                                                 init__r342 -> (Unknown int([0,1]),[0,1])
                                                 init__tmp___7 -> (Unknown int([0,7]),[0,1])
                                                 init__r412 -> (Unknown int([0,1]),[0,1])
                                                 init__tmp___8 -> (Unknown int([0,7]),[0,1])
                                                 init__r422 -> (Unknown int([0,1]),[0,1])
                                                 init__tmp___9 -> (Unknown int([0,7]),[0,1])
                                                 init__r432 -> (Unknown int([0,1]),[0,1])
                                                 init__tmp___10 -> (Unknown int([0,7]),[0,1])
                                                 init__r123 -> (Not {0}([0,1]),[0,1])
                                                 init__tmp___11 -> (Unknown int([0,7]),[0,1])
                                                 init__r133 -> (Not {0}([0,1]),[0,1])
                                                 init__tmp___12 -> (Unknown int([0,7]),[0,1])
                                                 init__r143 -> (Not {0}([0,1]),[0,1])
                                                 init__tmp___13 -> (Unknown int([0,7]),[0,1])
                                                 init__r213 -> (Not {0}([0,1]),[0,1])
                                                 init__tmp___14 -> (Unknown int([0,7]),[0,1])
                                                 init__r233 -> (Not {0}([0,1]),[0,1])
                                                 init__tmp___15 -> (Unknown int([0,7]),[0,1])
                                                 init__r243 -> (Not {0}([0,1]),[0,1])
                                                 init__tmp___16 -> (Unknown int([0,7]),[0,1])
                                                 init__r313 -> (Not {0}([0,1]),[0,1])
                                                 init__tmp___17 -> (Unknown int([0,7]),[0,1])
                                                 init__r323 -> (Not {0}([0,1]),[0,1])
                                                 init__tmp___18 -> (Unknown int([0,7]),[0,1])
                                                 init__r343 -> (Not {0}([0,1]),[0,1])
                                                 init__tmp___19 -> (Unknown int([0,7]),[0,1])
                                                 init__r413 -> (Not {0}([0,1]),[0,1])
                                                 init__tmp___20 -> (Unknown int([0,7]),[0,1])
                                                 init__r423 -> (Not {0}([0,1]),[0,1])
                                                 init__tmp___21 -> (Unknown int([0,7]),[0,1])
                                                 init__r433 -> (Not {0}([0,1]),[0,1])
                                                 init__tmp___22 -> (Unknown int([0,7]),[0,1])
                                                 init__tmp___23 -> (1,[1,1])
                                                 node1__newmax -> (Unknown int([0,7]),[0,1])
                                                 node2__newmax -> (Unknown int([0,7]),[0,1])
                                                 node3__newmax -> (Unknown int([0,7]),[0,1])
                                                 node4__newmax -> (Unknown int([0,7]),[0,1])
                                                 check__tmp -> (Unknown int([0,7]),[0,1])
                                                 __tmp_1 -> (Unknown int([0,1]),[0,1])
                                                 assert__arg -> (Unknown int([0,1]),[0,1])
                                                 node4____CPAchecker_TMP_0 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                 node4____CPAchecker_TMP_1 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                 node4____CPAchecker_TMP_2 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                 node3____CPAchecker_TMP_0 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                 node3____CPAchecker_TMP_1 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                 node3____CPAchecker_TMP_2 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                 node2____CPAchecker_TMP_0 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                 node2____CPAchecker_TMP_1 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                 node2____CPAchecker_TMP_2 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                 node1____CPAchecker_TMP_0 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                 node1____CPAchecker_TMP_1 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                 node1____CPAchecker_TMP_2 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                               }
                                               Global {
                                                 main -> (Unknown int([0,1]),[0,1])
                                               }
                                             }, mapping {
                                                    }),
     lifted proglines:Unknown line] -> {((node 500 "assert__arg = __tmp_1;", [Topped Set (variables):{},
                                                                              lifted regmap:mapping {
                                                                                              },
                                                                              Reversed (Topped Set (Cil expressions)):{},
                                                                              Topped Set (Set (Cil expressions)):{},
                                                                              Unit:(),
                                                                              Topped Set (variables):{},
                                                                              Reversed (Topped Set (Normal Lvals * booleans)):{},
                                                                              MT mode:Singlethreaded,
                                                                              Thread:main,
                                                                              value domain * array partitioning deps:(mapping {
                                                                                                                        Global {
                                                                                                                          __return_main -> (0,[0,0])
                                                                                                                          nomsg -> (-1,[-1,-1])
                                                                                                                          p12 -> (0,[0,0])
                                                                                                                          p12_old -> (0,[0,0])
                                                                                                                          p12_new -> (0,[0,0])
                                                                                                                          ep12 -> (0,[0,0])
                                                                                                                          p13 -> (0,[0,0])
                                                                                                                          p13_old -> (0,[0,0])
                                                                                                                          p13_new -> (0,[0,0])
                                                                                                                          ep13 -> (0,[0,0])
                                                                                                                          p14 -> (0,[0,0])
                                                                                                                          p14_old -> (0,[0,0])
                                                                                                                          p14_new -> (0,[0,0])
                                                                                                                          ep14 -> (0,[0,0])
                                                                                                                          p21 -> (0,[0,0])
                                                                                                                          p21_old -> (0,[0,0])
                                                                                                                          p21_new -> (0,[0,0])
                                                                                                                          ep21 -> (0,[0,0])
                                                                                                                          p23 -> (0,[0,0])
                                                                                                                          p23_old -> (0,[0,0])
                                                                                                                          p23_new -> (0,[0,0])
                                                                                                                          ep23 -> (0,[0,0])
                                                                                                                          p24 -> (0,[0,0])
                                                                                                                          p24_old -> (0,[0,0])
                                                                                                                          p24_new -> (0,[0,0])
                                                                                                                          ep24 -> (0,[0,0])
                                                                                                                          p31 -> (0,[0,0])
                                                                                                                          p31_old -> (0,[0,0])
                                                                                                                          p31_new -> (0,[0,0])
                                                                                                                          ep31 -> (0,[0,0])
                                                                                                                          p32 -> (0,[0,0])
                                                                                                                          p32_old -> (0,[0,0])
                                                                                                                          p32_new -> (0,[0,0])
                                                                                                                          ep32 -> (0,[0,0])
                                                                                                                          p34 -> (0,[0,0])
                                                                                                                          p34_old -> (0,[0,0])
                                                                                                                          p34_new -> (0,[0,0])
                                                                                                                          ep34 -> (0,[0,0])
                                                                                                                          p41 -> (0,[0,0])
                                                                                                                          p41_old -> (0,[0,0])
                                                                                                                          p41_new -> (0,[0,0])
                                                                                                                          ep41 -> (0,[0,0])
                                                                                                                          p42 -> (0,[0,0])
                                                                                                                          p42_old -> (0,[0,0])
                                                                                                                          p42_new -> (0,[0,0])
                                                                                                                          ep42 -> (0,[0,0])
                                                                                                                          p43 -> (0,[0,0])
                                                                                                                          p43_old -> (0,[0,0])
                                                                                                                          p43_new -> (0,[0,0])
                                                                                                                          ep43 -> (0,[0,0])
                                                                                                                          id1 -> (0,[0,0])
                                                                                                                          r1 -> (0,[0,0])
                                                                                                                          st1 -> (0,[0,0])
                                                                                                                          nl1 -> (0,[0,0])
                                                                                                                          m1 -> (0,[0,0])
                                                                                                                          max1 -> (0,[0,0])
                                                                                                                          mode1 -> (0,[0,0])
                                                                                                                          newmax1 -> (0,[0,0])
                                                                                                                          id2 -> (0,[0,0])
                                                                                                                          r2 -> (0,[0,0])
                                                                                                                          st2 -> (0,[0,0])
                                                                                                                          nl2 -> (0,[0,0])
                                                                                                                          m2 -> (0,[0,0])
                                                                                                                          max2 -> (0,[0,0])
                                                                                                                          mode2 -> (0,[0,0])
                                                                                                                          newmax2 -> (0,[0,0])
                                                                                                                          id3 -> (0,[0,0])
                                                                                                                          r3 -> (0,[0,0])
                                                                                                                          st3 -> (0,[0,0])
                                                                                                                          nl3 -> (0,[0,0])
                                                                                                                          m3 -> (0,[0,0])
                                                                                                                          max3 -> (0,[0,0])
                                                                                                                          mode3 -> (0,[0,0])
                                                                                                                          newmax3 -> (0,[0,0])
                                                                                                                          id4 -> (0,[0,0])
                                                                                                                          r4 -> (0,[0,0])
                                                                                                                          st4 -> (0,[0,0])
                                                                                                                          nl4 -> (0,[0,0])
                                                                                                                          m4 -> (0,[0,0])
                                                                                                                          max4 -> (0,[0,0])
                                                                                                                          mode4 -> (0,[0,0])
                                                                                                                          newmax4 -> (0,[0,0])
                                                                                                                          nodes -> 
                                                                                                                            (Array: Array (no part.): {&node1, &node2, &node3, &node4}, (Error int,bottom))
                                                                                                                          __return_3435 -> (0,[0,0])
                                                                                                                          __return_3681 -> (0,[0,0])
                                                                                                                        }
                                                                                                                      }, mapping {
                                                                                                                             }),
                                                                              lifted proglines:Unknown line], [Topped Set (variables):{},
                                                                                                               lifted regmap:mapping {
                                                                                                                               },
                                                                                                               Reversed (Topped Set (Cil expressions)):{},
                                                                                                               Topped Set (Set (Cil expressions)):{{0, main__i2}, {__tmp_1, main__c1}, {init__r122, init__tmp}, {init__r123, init__tmp___11}, {init__r132, init__tmp___0}, {init__r133, init__tmp___12}, {init__r142, init__tmp___1}, {init__r143, init__tmp___13}, {init__r212, init__tmp___2}, {init__r213, init__tmp___14}, {init__r232, init__tmp___3}, {init__r233, init__tmp___15}, {init__r242, init__tmp___4}, {init__r243, init__tmp___16}, {init__r312, init__tmp___5}, {init__r313, init__tmp___17}, {init__r322, init__tmp___6}, {init__r323, init__tmp___18}, {init__r342, init__tmp___7}, {init__r343, init__tmp___19}, {init__r412, init__tmp___8}, {init__r413, init__tmp___20}, {init__r422, init__tmp___9}, {init__r423, init__tmp___21}, {init__r432, init__tmp___10}, {init__r433, init__tmp___22}},
                                                                                                               Unit:(),
                                                                                                               Topped Set (variables):{},
                                                                                                               Reversed (Topped Set (Normal Lvals * booleans)):{},
                                                                                                               MT mode:Singlethreaded,
                                                                                                               Thread:main,
                                                                                                               value domain * array partitioning deps:(mapping {
                                                                                                                                                         Global {
                                                                                                                                                           __return_main -> (0,[0,0])
                                                                                                                                                           nomsg -> (-1,[-1,-1])
                                                                                                                                                           p12 -> (0,[0,0])
                                                                                                                                                           p12_old -> (Unknown int([-7,7]),[-1,127])
                                                                                                                                                           p12_new -> (-1,[-1,-1])
                                                                                                                                                           ep12 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           p13 -> (0,[0,0])
                                                                                                                                                           p13_old -> (Unknown int([-7,7]),[-1,127])
                                                                                                                                                           p13_new -> (-1,[-1,-1])
                                                                                                                                                           ep13 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           p14 -> (0,[0,0])
                                                                                                                                                           p14_old -> (Unknown int([-7,7]),[-1,127])
                                                                                                                                                           p14_new -> (-1,[-1,-1])
                                                                                                                                                           ep14 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           p21 -> (0,[0,0])
                                                                                                                                                           p21_old -> (Unknown int([-7,7]),[-1,127])
                                                                                                                                                           p21_new -> (-1,[-1,-1])
                                                                                                                                                           ep21 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           p23 -> (0,[0,0])
                                                                                                                                                           p23_old -> (Unknown int([-7,7]),[-1,127])
                                                                                                                                                           p23_new -> (-1,[-1,-1])
                                                                                                                                                           ep23 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           p24 -> (0,[0,0])
                                                                                                                                                           p24_old -> (Unknown int([-7,7]),[-1,127])
                                                                                                                                                           p24_new -> (-1,[-1,-1])
                                                                                                                                                           ep24 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           p31 -> (0,[0,0])
                                                                                                                                                           p31_old -> (Unknown int([-7,7]),[-1,127])
                                                                                                                                                           p31_new -> (-1,[-1,-1])
                                                                                                                                                           ep31 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           p32 -> (0,[0,0])
                                                                                                                                                           p32_old -> (Unknown int([-7,7]),[-1,127])
                                                                                                                                                           p32_new -> (-1,[-1,-1])
                                                                                                                                                           ep32 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           p34 -> (0,[0,0])
                                                                                                                                                           p34_old -> (Unknown int([-7,7]),[-1,127])
                                                                                                                                                           p34_new -> (-1,[-1,-1])
                                                                                                                                                           ep34 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           p41 -> (0,[0,0])
                                                                                                                                                           p41_old -> (Unknown int([-7,7]),[-1,127])
                                                                                                                                                           p41_new -> (-1,[-1,-1])
                                                                                                                                                           ep41 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           p42 -> (0,[0,0])
                                                                                                                                                           p42_old -> (Unknown int([-7,7]),[-1,127])
                                                                                                                                                           p42_new -> (-1,[-1,-1])
                                                                                                                                                           ep42 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           p43 -> (0,[0,0])
                                                                                                                                                           p43_old -> (Unknown int([-7,7]),[-1,127])
                                                                                                                                                           p43_new -> (-1,[-1,-1])
                                                                                                                                                           ep43 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           id1 -> (Unknown int([-7,7]),[0,127])
                                                                                                                                                           r1 -> (Unknown int([0,8]),[0,255])
                                                                                                                                                           st1 -> (Unknown int([0,7]),[0,127])
                                                                                                                                                           nl1 -> (Unknown int([0,7]),[0,127])
                                                                                                                                                           m1 -> (Unknown int([-7,7]),[-128,127])
                                                                                                                                                           max1 -> (Unknown int([-7,7]),[0,127])
                                                                                                                                                           mode1 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           newmax1 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           id2 -> (Unknown int([-7,7]),[0,127])
                                                                                                                                                           r2 -> (Unknown int([0,8]),[0,255])
                                                                                                                                                           st2 -> (Unknown int([0,7]),[0,127])
                                                                                                                                                           nl2 -> (Unknown int([0,7]),[0,127])
                                                                                                                                                           m2 -> (Unknown int([-7,7]),[-128,127])
                                                                                                                                                           max2 -> (Unknown int([-7,7]),[0,127])
                                                                                                                                                           mode2 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           newmax2 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           id3 -> (Unknown int([-7,7]),[0,127])
                                                                                                                                                           r3 -> (Unknown int([0,8]),[0,255])
                                                                                                                                                           st3 -> (Unknown int([0,7]),[0,127])
                                                                                                                                                           nl3 -> (Unknown int([0,7]),[0,127])
                                                                                                                                                           m3 -> (Unknown int([-7,7]),[-128,127])
                                                                                                                                                           max3 -> (Unknown int([-7,7]),[0,127])
                                                                                                                                                           mode3 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           newmax3 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           id4 -> (Unknown int([-7,7]),[0,127])
                                                                                                                                                           r4 -> (Unknown int([0,8]),[0,255])
                                                                                                                                                           st4 -> (Unknown int([0,7]),[0,127])
                                                                                                                                                           nl4 -> (Unknown int([0,7]),[0,127])
                                                                                                                                                           m4 -> (Unknown int([-7,7]),[-128,127])
                                                                                                                                                           max4 -> (Unknown int([-7,7]),[0,127])
                                                                                                                                                           mode4 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           newmax4 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           nodes -> 
                                                                                                                                                             (Array: Array (no part.): {&node1, &node2, &node3, &node4}, (Error int,bottom))
                                                                                                                                                           __return_3435 -> (1,[1,1])
                                                                                                                                                           __return_3681 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                         }
                                                                                                                                                         Local {
                                                                                                                                                           main__c1 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           main__i2 -> (0,[0,0])
                                                                                                                                                           init__r121 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__r131 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__r141 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__r211 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__r231 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__r241 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__r311 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__r321 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__r341 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__r411 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__r421 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__r431 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__r122 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__tmp -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r132 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__tmp___0 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r142 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__tmp___1 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r212 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__tmp___2 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r232 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__tmp___3 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r242 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__tmp___4 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r312 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__tmp___5 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r322 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__tmp___6 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r342 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__tmp___7 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r412 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__tmp___8 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r422 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__tmp___9 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r432 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__tmp___10 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r123 -> (Not {0}([0,1]),[0,1])
                                                                                                                                                           init__tmp___11 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r133 -> (Not {0}([0,1]),[0,1])
                                                                                                                                                           init__tmp___12 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r143 -> (Not {0}([0,1]),[0,1])
                                                                                                                                                           init__tmp___13 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r213 -> (Not {0}([0,1]),[0,1])
                                                                                                                                                           init__tmp___14 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r233 -> (Not {0}([0,1]),[0,1])
                                                                                                                                                           init__tmp___15 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r243 -> (Not {0}([0,1]),[0,1])
                                                                                                                                                           init__tmp___16 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r313 -> (Not {0}([0,1]),[0,1])
                                                                                                                                                           init__tmp___17 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r323 -> (Not {0}([0,1]),[0,1])
                                                                                                                                                           init__tmp___18 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r343 -> (Not {0}([0,1]),[0,1])
                                                                                                                                                           init__tmp___19 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r413 -> (Not {0}([0,1]),[0,1])
                                                                                                                                                           init__tmp___20 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r423 -> (Not {0}([0,1]),[0,1])
                                                                                                                                                           init__tmp___21 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r433 -> (Not {0}([0,1]),[0,1])
                                                                                                                                                           init__tmp___22 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__tmp___23 -> (1,[1,1])
                                                                                                                                                           node1__newmax -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           node2__newmax -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           node3__newmax -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           node4__newmax -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           check__tmp -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           __tmp_1 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           assert__arg -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           node4____CPAchecker_TMP_0 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                                                                                           node4____CPAchecker_TMP_1 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                                                                                           node4____CPAchecker_TMP_2 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                                                                                           node3____CPAchecker_TMP_0 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                                                                                           node3____CPAchecker_TMP_1 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                                                                                           node3____CPAchecker_TMP_2 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                                                                                           node2____CPAchecker_TMP_0 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                                                                                           node2____CPAchecker_TMP_1 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                                                                                           node2____CPAchecker_TMP_2 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                                                                                           node1____CPAchecker_TMP_0 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                                                                                           node1____CPAchecker_TMP_1 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                                                                                           node1____CPAchecker_TMP_2 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                                                                                         }
                                                                                                                                                         Global {
                                                                                                                                                           main -> (Unknown int([0,1]),[0,1])
                                                                                                                                                         }
                                                                                                                                                       }, mapping {
                                                                                                                                                              }),
                                                                                                               lifted proglines:Unknown line]), Assign 'assert__arg = __tmp_1' )}
  }, mapping {
         })
 Right-Hand-Side:
 (mapping {
    [Topped Set (variables):{}, lifted regmap:mapping {
                                                },
     Reversed (Topped Set (Cil expressions)):{},
     Topped Set (Set (Cil expressions)):{{__tmp_1, assert__arg, main__c1}, {init__r122, init__tmp}, {init__r123, init__tmp___11}, {init__r132, init__tmp___0}, {init__r133, init__tmp___12}, {init__r142, init__tmp___1}, {init__r143, init__tmp___13}, {init__r212, init__tmp___2}, {init__r213, init__tmp___14}, {init__r232, init__tmp___3}, {init__r233, init__tmp___15}, {init__r242, init__tmp___4}, {init__r243, init__tmp___16}, {init__r312, init__tmp___5}, {init__r313, init__tmp___17}, {init__r322, init__tmp___6}, {init__r323, init__tmp___18}, {init__r342, init__tmp___7}, {init__r343, init__tmp___19}, {init__r412, init__tmp___8}, {init__r413, init__tmp___20}, {init__r422, init__tmp___9}, {init__r423, init__tmp___21}, {init__r432, init__tmp___10}, {init__r433, init__tmp___22}},
     Unit:(), Topped Set (variables):{},
     Reversed (Topped Set (Normal Lvals * booleans)):{}, MT mode:Singlethreaded,
     Thread:main,
     value domain * array partitioning deps:(mapping {
                                               Global {
                                                 __return_main -> (0,[0,0])
                                                 nomsg -> (-1,[-1,-1])
                                                 p12 -> (0,[0,0])
                                                 p12_old -> (Unknown int([-7,7]),[-1,127])
                                                 p12_new -> (-1,[-1,-1])
                                                 ep12 -> (Unknown int([0,1]),[0,1])
                                                 p13 -> (0,[0,0])
                                                 p13_old -> (Unknown int([-7,7]),[-1,127])
                                                 p13_new -> (-1,[-1,-1])
                                                 ep13 -> (Unknown int([0,1]),[0,1])
                                                 p14 -> (0,[0,0])
                                                 p14_old -> (Unknown int([-7,7]),[-1,127])
                                                 p14_new -> (-1,[-1,-1])
                                                 ep14 -> (Unknown int([0,1]),[0,1])
                                                 p21 -> (0,[0,0])
                                                 p21_old -> (Unknown int([-7,7]),[-1,127])
                                                 p21_new -> (-1,[-1,-1])
                                                 ep21 -> (Unknown int([0,1]),[0,1])
                                                 p23 -> (0,[0,0])
                                                 p23_old -> (Unknown int([-7,7]),[-1,127])
                                                 p23_new -> (-1,[-1,-1])
                                                 ep23 -> (Unknown int([0,1]),[0,1])
                                                 p24 -> (0,[0,0])
                                                 p24_old -> (Unknown int([-7,7]),[-1,127])
                                                 p24_new -> (-1,[-1,-1])
                                                 ep24 -> (Unknown int([0,1]),[0,1])
                                                 p31 -> (0,[0,0])
                                                 p31_old -> (Unknown int([-7,7]),[-1,127])
                                                 p31_new -> (-1,[-1,-1])
                                                 ep31 -> (Unknown int([0,1]),[0,1])
                                                 p32 -> (0,[0,0])
                                                 p32_old -> (Unknown int([-7,7]),[-1,127])
                                                 p32_new -> (-1,[-1,-1])
                                                 ep32 -> (Unknown int([0,1]),[0,1])
                                                 p34 -> (0,[0,0])
                                                 p34_old -> (Unknown int([-7,7]),[-1,127])
                                                 p34_new -> (-1,[-1,-1])
                                                 ep34 -> (Unknown int([0,1]),[0,1])
                                                 p41 -> (0,[0,0])
                                                 p41_old -> (Unknown int([-7,7]),[-1,127])
                                                 p41_new -> (-1,[-1,-1])
                                                 ep41 -> (Unknown int([0,1]),[0,1])
                                                 p42 -> (0,[0,0])
                                                 p42_old -> (Unknown int([-7,7]),[-1,127])
                                                 p42_new -> (-1,[-1,-1])
                                                 ep42 -> (Unknown int([0,1]),[0,1])
                                                 p43 -> (0,[0,0])
                                                 p43_old -> (Unknown int([-7,7]),[-1,127])
                                                 p43_new -> (-1,[-1,-1])
                                                 ep43 -> (Unknown int([0,1]),[0,1])
                                                 id1 -> (Unknown int([-7,7]),[0,127])
                                                 r1 -> (Unknown int([0,8]),[0,255])
                                                 st1 -> (Unknown int([0,7]),[0,127])
                                                 nl1 -> (Unknown int([0,7]),[0,127])
                                                 m1 -> (Unknown int([-7,7]),[-128,127])
                                                 max1 -> (Unknown int([-7,7]),[0,127])
                                                 mode1 -> (Unknown int([0,7]),[0,1])
                                                 newmax1 -> (Unknown int([0,1]),[0,1])
                                                 id2 -> (Unknown int([-7,7]),[0,127])
                                                 r2 -> (Unknown int([0,8]),[0,255])
                                                 st2 -> (Unknown int([0,7]),[0,127])
                                                 nl2 -> (Unknown int([0,7]),[0,127])
                                                 m2 -> (Unknown int([-7,7]),[-128,127])
                                                 max2 -> (Unknown int([-7,7]),[0,127])
                                                 mode2 -> (Unknown int([0,7]),[0,1])
                                                 newmax2 -> (Unknown int([0,1]),[0,1])
                                                 id3 -> (Unknown int([-7,7]),[0,127])
                                                 r3 -> (Unknown int([0,8]),[0,255])
                                                 st3 -> (Unknown int([0,7]),[0,127])
                                                 nl3 -> (Unknown int([0,7]),[0,127])
                                                 m3 -> (Unknown int([-7,7]),[-128,127])
                                                 max3 -> (Unknown int([-7,7]),[0,127])
                                                 mode3 -> (Unknown int([0,7]),[0,1])
                                                 newmax3 -> (Unknown int([0,1]),[0,1])
                                                 id4 -> (Unknown int([-7,7]),[0,127])
                                                 r4 -> (Unknown int([0,8]),[0,255])
                                                 st4 -> (Unknown int([0,7]),[0,127])
                                                 nl4 -> (Unknown int([0,7]),[0,127])
                                                 m4 -> (Unknown int([-7,7]),[-128,127])
                                                 max4 -> (Unknown int([-7,7]),[0,127])
                                                 mode4 -> (Unknown int([0,7]),[0,1])
                                                 newmax4 -> (Unknown int([0,1]),[0,1])
                                                 nodes -> 
                                                   (Array: Array (no part.): {&node1, &node2, &node3, &node4}, (Error int,bottom))
                                                 __return_3435 -> (1,[1,1])
                                                 __return_3681 -> (Unknown int([0,7]),[0,1])
                                               }
                                               Local {
                                                 main__c1 -> (Unknown int([0,7]),[0,1])
                                                 main__i2 -> (0,[0,0])
                                                 init__r121 -> (Unknown int([0,1]),[0,1])
                                                 init__r131 -> (Unknown int([0,1]),[0,1])
                                                 init__r141 -> (Unknown int([0,1]),[0,1])
                                                 init__r211 -> (Unknown int([0,1]),[0,1])
                                                 init__r231 -> (Unknown int([0,1]),[0,1])
                                                 init__r241 -> (Unknown int([0,1]),[0,1])
                                                 init__r311 -> (Unknown int([0,1]),[0,1])
                                                 init__r321 -> (Unknown int([0,1]),[0,1])
                                                 init__r341 -> (Unknown int([0,1]),[0,1])
                                                 init__r411 -> (Unknown int([0,1]),[0,1])
                                                 init__r421 -> (Unknown int([0,1]),[0,1])
                                                 init__r431 -> (Unknown int([0,1]),[0,1])
                                                 init__r122 -> (Unknown int([0,1]),[0,1])
                                                 init__tmp -> (Unknown int([0,7]),[0,1])
                                                 init__r132 -> (Unknown int([0,1]),[0,1])
                                                 init__tmp___0 -> (Unknown int([0,7]),[0,1])
                                                 init__r142 -> (Unknown int([0,1]),[0,1])
                                                 init__tmp___1 -> (Unknown int([0,7]),[0,1])
                                                 init__r212 -> (Unknown int([0,1]),[0,1])
                                                 init__tmp___2 -> (Unknown int([0,7]),[0,1])
                                                 init__r232 -> (Unknown int([0,1]),[0,1])
                                                 init__tmp___3 -> (Unknown int([0,7]),[0,1])
                                                 init__r242 -> (Unknown int([0,1]),[0,1])
                                                 init__tmp___4 -> (Unknown int([0,7]),[0,1])
                                                 init__r312 -> (Unknown int([0,1]),[0,1])
                                                 init__tmp___5 -> (Unknown int([0,7]),[0,1])
                                                 init__r322 -> (Unknown int([0,1]),[0,1])
                                                 init__tmp___6 -> (Unknown int([0,7]),[0,1])
                                                 init__r342 -> (Unknown int([0,1]),[0,1])
                                                 init__tmp___7 -> (Unknown int([0,7]),[0,1])
                                                 init__r412 -> (Unknown int([0,1]),[0,1])
                                                 init__tmp___8 -> (Unknown int([0,7]),[0,1])
                                                 init__r422 -> (Unknown int([0,1]),[0,1])
                                                 init__tmp___9 -> (Unknown int([0,7]),[0,1])
                                                 init__r432 -> (Unknown int([0,1]),[0,1])
                                                 init__tmp___10 -> (Unknown int([0,7]),[0,1])
                                                 init__r123 -> (Not {0}([0,1]),[0,1])
                                                 init__tmp___11 -> (Unknown int([0,7]),[0,1])
                                                 init__r133 -> (Not {0}([0,1]),[0,1])
                                                 init__tmp___12 -> (Unknown int([0,7]),[0,1])
                                                 init__r143 -> (Not {0}([0,1]),[0,1])
                                                 init__tmp___13 -> (Unknown int([0,7]),[0,1])
                                                 init__r213 -> (Not {0}([0,1]),[0,1])
                                                 init__tmp___14 -> (Unknown int([0,7]),[0,1])
                                                 init__r233 -> (Not {0}([0,1]),[0,1])
                                                 init__tmp___15 -> (Unknown int([0,7]),[0,1])
                                                 init__r243 -> (Not {0}([0,1]),[0,1])
                                                 init__tmp___16 -> (Unknown int([0,7]),[0,1])
                                                 init__r313 -> (Not {0}([0,1]),[0,1])
                                                 init__tmp___17 -> (Unknown int([0,7]),[0,1])
                                                 init__r323 -> (Not {0}([0,1]),[0,1])
                                                 init__tmp___18 -> (Unknown int([0,7]),[0,1])
                                                 init__r343 -> (Not {0}([0,1]),[0,1])
                                                 init__tmp___19 -> (Unknown int([0,7]),[0,1])
                                                 init__r413 -> (Not {0}([0,1]),[0,1])
                                                 init__tmp___20 -> (Unknown int([0,7]),[0,1])
                                                 init__r423 -> (Not {0}([0,1]),[0,1])
                                                 init__tmp___21 -> (Unknown int([0,7]),[0,1])
                                                 init__r433 -> (Not {0}([0,1]),[0,1])
                                                 init__tmp___22 -> (Unknown int([0,7]),[0,1])
                                                 init__tmp___23 -> (1,[1,1])
                                                 node1__newmax -> (Unknown int([0,7]),[0,1])
                                                 node2__newmax -> (Unknown int([0,7]),[0,1])
                                                 node3__newmax -> (Unknown int([0,7]),[0,1])
                                                 node4__newmax -> (Unknown int([0,7]),[0,1])
                                                 check__tmp -> (Unknown int([0,7]),[0,1])
                                                 __tmp_1 -> (Unknown int([0,1]),[0,1])
                                                 assert__arg -> (Unknown int([0,1]),[0,1])
                                                 node4____CPAchecker_TMP_0 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                 node4____CPAchecker_TMP_1 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                 node4____CPAchecker_TMP_2 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                 node3____CPAchecker_TMP_0 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                 node3____CPAchecker_TMP_1 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                 node3____CPAchecker_TMP_2 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                 node2____CPAchecker_TMP_0 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                 node2____CPAchecker_TMP_1 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                 node2____CPAchecker_TMP_2 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                 node1____CPAchecker_TMP_0 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                 node1____CPAchecker_TMP_1 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                 node1____CPAchecker_TMP_2 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                               }
                                               Global {
                                                 main -> (Unknown int([0,1]),[0,1])
                                               }
                                             }, mapping {
                                                    }),
     lifted proglines:Unknown line] -> {((node 500 "assert__arg = __tmp_1;", [Topped Set (variables):{},
                                                                              lifted regmap:mapping {
                                                                                              },
                                                                              Reversed (Topped Set (Cil expressions)):{},
                                                                              Topped Set (Set (Cil expressions)):{},
                                                                              Unit:(),
                                                                              Topped Set (variables):{},
                                                                              Reversed (Topped Set (Normal Lvals * booleans)):{},
                                                                              MT mode:Singlethreaded,
                                                                              Thread:main,
                                                                              value domain * array partitioning deps:(mapping {
                                                                                                                        Global {
                                                                                                                          __return_main -> (0,[0,0])
                                                                                                                          nomsg -> (-1,[-1,-1])
                                                                                                                          p12 -> (0,[0,0])
                                                                                                                          p12_old -> (0,[0,0])
                                                                                                                          p12_new -> (0,[0,0])
                                                                                                                          ep12 -> (0,[0,0])
                                                                                                                          p13 -> (0,[0,0])
                                                                                                                          p13_old -> (0,[0,0])
                                                                                                                          p13_new -> (0,[0,0])
                                                                                                                          ep13 -> (0,[0,0])
                                                                                                                          p14 -> (0,[0,0])
                                                                                                                          p14_old -> (0,[0,0])
                                                                                                                          p14_new -> (0,[0,0])
                                                                                                                          ep14 -> (0,[0,0])
                                                                                                                          p21 -> (0,[0,0])
                                                                                                                          p21_old -> (0,[0,0])
                                                                                                                          p21_new -> (0,[0,0])
                                                                                                                          ep21 -> (0,[0,0])
                                                                                                                          p23 -> (0,[0,0])
                                                                                                                          p23_old -> (0,[0,0])
                                                                                                                          p23_new -> (0,[0,0])
                                                                                                                          ep23 -> (0,[0,0])
                                                                                                                          p24 -> (0,[0,0])
                                                                                                                          p24_old -> (0,[0,0])
                                                                                                                          p24_new -> (0,[0,0])
                                                                                                                          ep24 -> (0,[0,0])
                                                                                                                          p31 -> (0,[0,0])
                                                                                                                          p31_old -> (0,[0,0])
                                                                                                                          p31_new -> (0,[0,0])
                                                                                                                          ep31 -> (0,[0,0])
                                                                                                                          p32 -> (0,[0,0])
                                                                                                                          p32_old -> (0,[0,0])
                                                                                                                          p32_new -> (0,[0,0])
                                                                                                                          ep32 -> (0,[0,0])
                                                                                                                          p34 -> (0,[0,0])
                                                                                                                          p34_old -> (0,[0,0])
                                                                                                                          p34_new -> (0,[0,0])
                                                                                                                          ep34 -> (0,[0,0])
                                                                                                                          p41 -> (0,[0,0])
                                                                                                                          p41_old -> (0,[0,0])
                                                                                                                          p41_new -> (0,[0,0])
                                                                                                                          ep41 -> (0,[0,0])
                                                                                                                          p42 -> (0,[0,0])
                                                                                                                          p42_old -> (0,[0,0])
                                                                                                                          p42_new -> (0,[0,0])
                                                                                                                          ep42 -> (0,[0,0])
                                                                                                                          p43 -> (0,[0,0])
                                                                                                                          p43_old -> (0,[0,0])
                                                                                                                          p43_new -> (0,[0,0])
                                                                                                                          ep43 -> (0,[0,0])
                                                                                                                          id1 -> (0,[0,0])
                                                                                                                          r1 -> (0,[0,0])
                                                                                                                          st1 -> (0,[0,0])
                                                                                                                          nl1 -> (0,[0,0])
                                                                                                                          m1 -> (0,[0,0])
                                                                                                                          max1 -> (0,[0,0])
                                                                                                                          mode1 -> (0,[0,0])
                                                                                                                          newmax1 -> (0,[0,0])
                                                                                                                          id2 -> (0,[0,0])
                                                                                                                          r2 -> (0,[0,0])
                                                                                                                          st2 -> (0,[0,0])
                                                                                                                          nl2 -> (0,[0,0])
                                                                                                                          m2 -> (0,[0,0])
                                                                                                                          max2 -> (0,[0,0])
                                                                                                                          mode2 -> (0,[0,0])
                                                                                                                          newmax2 -> (0,[0,0])
                                                                                                                          id3 -> (0,[0,0])
                                                                                                                          r3 -> (0,[0,0])
                                                                                                                          st3 -> (0,[0,0])
                                                                                                                          nl3 -> (0,[0,0])
                                                                                                                          m3 -> (0,[0,0])
                                                                                                                          max3 -> (0,[0,0])
                                                                                                                          mode3 -> (0,[0,0])
                                                                                                                          newmax3 -> (0,[0,0])
                                                                                                                          id4 -> (0,[0,0])
                                                                                                                          r4 -> (0,[0,0])
                                                                                                                          st4 -> (0,[0,0])
                                                                                                                          nl4 -> (0,[0,0])
                                                                                                                          m4 -> (0,[0,0])
                                                                                                                          max4 -> (0,[0,0])
                                                                                                                          mode4 -> (0,[0,0])
                                                                                                                          newmax4 -> (0,[0,0])
                                                                                                                          nodes -> 
                                                                                                                            (Array: Array (no part.): {&node1, &node2, &node3, &node4}, (Error int,bottom))
                                                                                                                          __return_3435 -> (0,[0,0])
                                                                                                                          __return_3681 -> (0,[0,0])
                                                                                                                        }
                                                                                                                      }, mapping {
                                                                                                                             }),
                                                                              lifted proglines:Unknown line], [Topped Set (variables):{},
                                                                                                               lifted regmap:mapping {
                                                                                                                               },
                                                                                                               Reversed (Topped Set (Cil expressions)):{},
                                                                                                               Topped Set (Set (Cil expressions)):{{__tmp_1, main__c1}, {init__r122, init__tmp}, {init__r123, init__tmp___11}, {init__r132, init__tmp___0}, {init__r133, init__tmp___12}, {init__r142, init__tmp___1}, {init__r143, init__tmp___13}, {init__r212, init__tmp___2}, {init__r213, init__tmp___14}, {init__r232, init__tmp___3}, {init__r233, init__tmp___15}, {init__r242, init__tmp___4}, {init__r243, init__tmp___16}, {init__r312, init__tmp___5}, {init__r313, init__tmp___17}, {init__r322, init__tmp___6}, {init__r323, init__tmp___18}, {init__r342, init__tmp___7}, {init__r343, init__tmp___19}, {init__r412, init__tmp___8}, {init__r413, init__tmp___20}, {init__r422, init__tmp___9}, {init__r423, init__tmp___21}, {init__r432, init__tmp___10}, {init__r433, init__tmp___22}},
                                                                                                               Unit:(),
                                                                                                               Topped Set (variables):{},
                                                                                                               Reversed (Topped Set (Normal Lvals * booleans)):{},
                                                                                                               MT mode:Singlethreaded,
                                                                                                               Thread:main,
                                                                                                               value domain * array partitioning deps:(mapping {
                                                                                                                                                         Global {
                                                                                                                                                           __return_main -> (0,[0,0])
                                                                                                                                                           nomsg -> (-1,[-1,-1])
                                                                                                                                                           p12 -> (0,[0,0])
                                                                                                                                                           p12_old -> (Unknown int([-7,7]),[-1,127])
                                                                                                                                                           p12_new -> (-1,[-1,-1])
                                                                                                                                                           ep12 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           p13 -> (0,[0,0])
                                                                                                                                                           p13_old -> (Unknown int([-7,7]),[-1,127])
                                                                                                                                                           p13_new -> (-1,[-1,-1])
                                                                                                                                                           ep13 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           p14 -> (0,[0,0])
                                                                                                                                                           p14_old -> (Unknown int([-7,7]),[-1,127])
                                                                                                                                                           p14_new -> (-1,[-1,-1])
                                                                                                                                                           ep14 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           p21 -> (0,[0,0])
                                                                                                                                                           p21_old -> (Unknown int([-7,7]),[-1,127])
                                                                                                                                                           p21_new -> (-1,[-1,-1])
                                                                                                                                                           ep21 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           p23 -> (0,[0,0])
                                                                                                                                                           p23_old -> (Unknown int([-7,7]),[-1,127])
                                                                                                                                                           p23_new -> (-1,[-1,-1])
                                                                                                                                                           ep23 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           p24 -> (0,[0,0])
                                                                                                                                                           p24_old -> (Unknown int([-7,7]),[-1,127])
                                                                                                                                                           p24_new -> (-1,[-1,-1])
                                                                                                                                                           ep24 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           p31 -> (0,[0,0])
                                                                                                                                                           p31_old -> (Unknown int([-7,7]),[-1,127])
                                                                                                                                                           p31_new -> (-1,[-1,-1])
                                                                                                                                                           ep31 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           p32 -> (0,[0,0])
                                                                                                                                                           p32_old -> (Unknown int([-7,7]),[-1,127])
                                                                                                                                                           p32_new -> (-1,[-1,-1])
                                                                                                                                                           ep32 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           p34 -> (0,[0,0])
                                                                                                                                                           p34_old -> (Unknown int([-7,7]),[-1,127])
                                                                                                                                                           p34_new -> (-1,[-1,-1])
                                                                                                                                                           ep34 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           p41 -> (0,[0,0])
                                                                                                                                                           p41_old -> (Unknown int([-7,7]),[-1,127])
                                                                                                                                                           p41_new -> (-1,[-1,-1])
                                                                                                                                                           ep41 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           p42 -> (0,[0,0])
                                                                                                                                                           p42_old -> (Unknown int([-7,7]),[-1,127])
                                                                                                                                                           p42_new -> (-1,[-1,-1])
                                                                                                                                                           ep42 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           p43 -> (0,[0,0])
                                                                                                                                                           p43_old -> (Unknown int([-7,7]),[-1,127])
                                                                                                                                                           p43_new -> (-1,[-1,-1])
                                                                                                                                                           ep43 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           id1 -> (Unknown int([-7,7]),[0,127])
                                                                                                                                                           r1 -> (Unknown int([0,8]),[0,255])
                                                                                                                                                           st1 -> (Unknown int([0,7]),[0,127])
                                                                                                                                                           nl1 -> (Unknown int([0,7]),[0,127])
                                                                                                                                                           m1 -> (Unknown int([-7,7]),[-128,127])
                                                                                                                                                           max1 -> (Unknown int([-7,7]),[0,127])
                                                                                                                                                           mode1 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           newmax1 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           id2 -> (Unknown int([-7,7]),[0,127])
                                                                                                                                                           r2 -> (Unknown int([0,8]),[0,255])
                                                                                                                                                           st2 -> (Unknown int([0,7]),[0,127])
                                                                                                                                                           nl2 -> (Unknown int([0,7]),[0,127])
                                                                                                                                                           m2 -> (Unknown int([-7,7]),[-128,127])
                                                                                                                                                           max2 -> (Unknown int([-7,7]),[0,127])
                                                                                                                                                           mode2 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           newmax2 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           id3 -> (Unknown int([-7,7]),[0,127])
                                                                                                                                                           r3 -> (Unknown int([0,8]),[0,255])
                                                                                                                                                           st3 -> (Unknown int([0,7]),[0,127])
                                                                                                                                                           nl3 -> (Unknown int([0,7]),[0,127])
                                                                                                                                                           m3 -> (Unknown int([-7,7]),[-128,127])
                                                                                                                                                           max3 -> (Unknown int([-7,7]),[0,127])
                                                                                                                                                           mode3 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           newmax3 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           id4 -> (Unknown int([-7,7]),[0,127])
                                                                                                                                                           r4 -> (Unknown int([0,8]),[0,255])
                                                                                                                                                           st4 -> (Unknown int([0,7]),[0,127])
                                                                                                                                                           nl4 -> (Unknown int([0,7]),[0,127])
                                                                                                                                                           m4 -> (Unknown int([-7,7]),[-128,127])
                                                                                                                                                           max4 -> (Unknown int([-7,7]),[0,127])
                                                                                                                                                           mode4 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           newmax4 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           nodes -> 
                                                                                                                                                             (Array: Array (no part.): {&node1, &node2, &node3, &node4}, (Error int,bottom))
                                                                                                                                                           __return_3435 -> (1,[1,1])
                                                                                                                                                           __return_3681 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                         }
                                                                                                                                                         Local {
                                                                                                                                                           main__c1 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           main__i2 -> (0,[0,0])
                                                                                                                                                           init__r121 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__r131 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__r141 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__r211 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__r231 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__r241 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__r311 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__r321 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__r341 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__r411 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__r421 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__r431 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__r122 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__tmp -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r132 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__tmp___0 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r142 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__tmp___1 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r212 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__tmp___2 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r232 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__tmp___3 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r242 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__tmp___4 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r312 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__tmp___5 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r322 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__tmp___6 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r342 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__tmp___7 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r412 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__tmp___8 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r422 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__tmp___9 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r432 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           init__tmp___10 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r123 -> (Not {0}([0,1]),[0,1])
                                                                                                                                                           init__tmp___11 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r133 -> (Not {0}([0,1]),[0,1])
                                                                                                                                                           init__tmp___12 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r143 -> (Not {0}([0,1]),[0,1])
                                                                                                                                                           init__tmp___13 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r213 -> (Not {0}([0,1]),[0,1])
                                                                                                                                                           init__tmp___14 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r233 -> (Not {0}([0,1]),[0,1])
                                                                                                                                                           init__tmp___15 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r243 -> (Not {0}([0,1]),[0,1])
                                                                                                                                                           init__tmp___16 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r313 -> (Not {0}([0,1]),[0,1])
                                                                                                                                                           init__tmp___17 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r323 -> (Not {0}([0,1]),[0,1])
                                                                                                                                                           init__tmp___18 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r343 -> (Not {0}([0,1]),[0,1])
                                                                                                                                                           init__tmp___19 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r413 -> (Not {0}([0,1]),[0,1])
                                                                                                                                                           init__tmp___20 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r423 -> (Not {0}([0,1]),[0,1])
                                                                                                                                                           init__tmp___21 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__r433 -> (Not {0}([0,1]),[0,1])
                                                                                                                                                           init__tmp___22 -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           init__tmp___23 -> (1,[1,1])
                                                                                                                                                           node1__newmax -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           node2__newmax -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           node3__newmax -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           node4__newmax -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           check__tmp -> (Unknown int([0,7]),[0,1])
                                                                                                                                                           __tmp_1 -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           assert__arg -> (Unknown int([0,1]),[0,1])
                                                                                                                                                           node4____CPAchecker_TMP_0 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                                                                                           node4____CPAchecker_TMP_1 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                                                                                           node4____CPAchecker_TMP_2 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                                                                                           node3____CPAchecker_TMP_0 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                                                                                           node3____CPAchecker_TMP_1 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                                                                                           node3____CPAchecker_TMP_2 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                                                                                           node2____CPAchecker_TMP_0 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                                                                                           node2____CPAchecker_TMP_1 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                                                                                           node2____CPAchecker_TMP_2 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                                                                                           node1____CPAchecker_TMP_0 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                                                                                           node1____CPAchecker_TMP_1 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                                                                                           node1____CPAchecker_TMP_2 -> (Unknown int([-31,31]),[-2147483648,2147483647])
                                                                                                                                                         }
                                                                                                                                                         Global {
                                                                                                                                                           main -> (Unknown int([0,1]),[0,1])
                                                                                                                                                         }
                                                                                                                                                       }, mapping {
                                                                                                                                                              }),
                                                                                                               lifted proglines:Unknown line]), Assign 'assert__arg = __tmp_1' )}
  }, mapping {
         })
 Difference: Set (Set (Cil expressions)): These are fine!. 
File '../../sv-comp/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c':
  function 'main' has dead code on lines: 912, 934, 956, 1077, 1099, 1121, 1242, 1264, 1286, 1407, 1429, 1451, 1479
Found dead code on 13 lines!
Dead code: the else branch over expression '(int )max4 != (int )nomsg' is dead! (../../sv-comp/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:912)
Dead code: the else branch over expression '(int )max4 != (int )nomsg' is dead! (../../sv-comp/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:934)
Dead code: the else branch over expression '(int )max4 != (int )nomsg' is dead! (../../sv-comp/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:956)
Dead code: the else branch over expression '(int )max3 != (int )nomsg' is dead! (../../sv-comp/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1077)
Dead code: the else branch over expression '(int )max3 != (int )nomsg' is dead! (../../sv-comp/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1099)
Dead code: the else branch over expression '(int )max3 != (int )nomsg' is dead! (../../sv-comp/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1121)
Dead code: the else branch over expression '(int )max2 != (int )nomsg' is dead! (../../sv-comp/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1242)
Dead code: the else branch over expression '(int )max2 != (int )nomsg' is dead! (../../sv-comp/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1264)
Dead code: the else branch over expression '(int )max2 != (int )nomsg' is dead! (../../sv-comp/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1286)
Dead code: the else branch over expression '(int )max1 != (int )nomsg' is dead! (../../sv-comp/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1407)
Dead code: the else branch over expression '(int )max1 != (int )nomsg' is dead! (../../sv-comp/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1429)
Dead code: the else branch over expression '(int )max1 != (int )nomsg' is dead! (../../sv-comp/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1451)
Dead code: the else branch over expression 'main__i2 != 0' is dead! (../../sv-comp/sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1479)
SV-COMP result: ERROR (verify)
Writing xml to temp. file: /tmp/ocaml6cb765tmp

Timings:
TOTAL                          36.244 s
  parse                           0.008 s
  convert to CIL                  0.008 s
  analysis                       36.229 s
    global_inits                    0.023 s
    solving                        16.905 s
      S.Dom.equal                     0.029 s
    verify                          4.179 s
    reachability                    3.793 s
    witness                         0.000 s
Timing used
Memory statistics: total=38432.33MB, max=58.97MB, minor=38429.26MB, major=180.19MB, promoted=177.12MB
    minor collections=18337  major collections=27 compactions=0
Time needed: 7446 ms

I think the message with Difference: Set (Set (Cil expressions)): These are fine!. is due to some functor not modifying pretty_diff despite changing leq.

The difference is

Solver computed:

Topped Set (Set (Cil expressions)):{{0, main__i2}, {__tmp_1, assert__arg, main__c1}, ....

RHS:

Topped Set (Set (Cil expressions)):{{__tmp_1, assert__arg, main__c1}, ...

@sim642
Copy link
Member

sim642 commented Dec 7, 2020

I can run the same command (with relative paths changed) and get a different result:

./goblint --conf conf/svcomp21.json --sets ana.specification ../sv-benchmarks/c/properties/unreach-call.prp --html  ../sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c
SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
File '../sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c':
  function 'main' has dead code on lines: 912, 934, 956, 1077, 1099, 1121, 1242, 1264, 1286, 1407, 1429, 1451, 1479
Found dead code on 13 lines!
Dead code: the else branch over expression '(int )max4 != (int )nomsg' is dead! (../sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:912)
Dead code: the else branch over expression '(int )max4 != (int )nomsg' is dead! (../sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:934)
Dead code: the else branch over expression '(int )max4 != (int )nomsg' is dead! (../sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:956)
Dead code: the else branch over expression '(int )max3 != (int )nomsg' is dead! (../sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1077)
Dead code: the else branch over expression '(int )max3 != (int )nomsg' is dead! (../sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1099)
Dead code: the else branch over expression '(int )max3 != (int )nomsg' is dead! (../sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1121)
Dead code: the else branch over expression '(int )max2 != (int )nomsg' is dead! (../sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1242)
Dead code: the else branch over expression '(int )max2 != (int )nomsg' is dead! (../sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1264)
Dead code: the else branch over expression '(int )max2 != (int )nomsg' is dead! (../sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1286)
Dead code: the else branch over expression '(int )max1 != (int )nomsg' is dead! (../sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1407)
Dead code: the else branch over expression '(int )max1 != (int )nomsg' is dead! (../sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1429)
Dead code: the else branch over expression '(int )max1 != (int )nomsg' is dead! (../sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1451)
Dead code: the else branch over expression 'main__i2 != 0' is dead! (../sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c:1479)
SV-COMP result: unknown
Writing xml to temp. file: /tmp/ocamla7250atmp

Timings:
TOTAL                          22.186 s
  parse                           0.010 s
  convert to CIL                  0.016 s
  analysis                       22.160 s
    global_inits                    0.008 s
    solving                        11.073 s
      S.Dom.equal                     0.020 s
    verify                          2.065 s
    reachability                    1.967 s
    witness                         1.914 s
      determine                       0.003 s
      write                           1.910 s
Timing used
Memory statistics: total=40548.70MB, max=58.97MB, minor=40501.04MB, major=250.22MB, promoted=202.56MB
    minor collections=19327  major collections=31 compactions=0
Time needed: 6604 ms

This is bizarre, I don't have any uncommited changes and have made a clean build.

@michael-schwarz
Copy link
Member Author

michael-schwarz commented Dec 8, 2020 •
edited
Loading

Strange indeed, after going back to an older commit and another make clean, I can also no longer observe this problem when I build from scratch.
However, if I use the binary from the release, this problem still happens (I tried with pals_opt-floodmax.5.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c).

Was the release maybe dirty?

michael-schwarz added a commit that referenced this issue Dec 8, 2020
@michael-schwarz
Sv-Comp: Add make clean and make to archive script. References #153
5a3a5de
@sim642
Copy link
Member

sim642 commented Dec 8, 2020

I don't think it was because I always made the archive build on our Ubuntu 20.04 server where I didn't do any development and also did it after make clean. Also, if it was dirty, then the version number would say -dirty.

@michael-schwarz
Copy link
Member Author

Can you reproduce it with the binary that we submitted?

@sim642
Copy link
Member

sim642 commented Dec 8, 2020

I will try that soon. It would be quite impossible to debug and fix it though if it somehow doesn't happen on new builds.

it might be a hint in itself as to where the issue is. Like maybe somewhere physical equality (==) is accidentally being used. Not sure what else could give such non-deterministic behavior.

@sim642
Copy link
Member

sim642 commented Dec 8, 2020

I tried with the exact executable from the verifier archive (SHA-256 below) and I still gives the unknown answer:

simmo@goblint-new:/mnt/goblint-svcomp/sv-comp/goblint$ sha256sum ./asd/goblint/goblint 
16574d3cacb6ab22b29fada00cdeecc14c74706cf6d90526e4068329616d3618  ./asd/goblint/goblint
simmo@goblint-new:/mnt/goblint-svcomp/sv-comp/goblint$ ./asd/goblint/goblint --conf conf/svcomp21.json --sets ana.specification ../sv-benchmarks/c/properties/unreach-call.prp ../sv-benchmarks/c/seq-mthreaded-reduced/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c
SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
SV-COMP result: unknown

Timings:
TOTAL                          13.621 s
  parse                           0.004 s
  convert to CIL                  0.004 s
  analysis                       13.614 s
    global_inits                    0.011 s
    solving                         9.102 s
      S.Dom.equal                     0.007 s
    verify                          1.838 s
    reachability                    1.729 s
    witness                         0.930 s
      determine                       0.002 s
      write                           0.928 s
Timing used
Memory statistics: total=25569.06MB, max=58.97MB, minor=25521.33MB, major=235.14MB, promoted=187.41MB
    minor collections=12184  major collections=29 compactions=0

@michael-schwarz
Copy link
Member Author

michael-schwarz commented Dec 8, 2020 •
edited
Loading

Can you try with pals_opt-floodmax.5.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c, too?
I still get the error with that (same sha256 as you posted above).

mbs@mbs-VirtualBox:~/Desktop/goblint$ sha256sum goblint
16574d3cacb6ab22b29fada00cdeecc14c74706cf6d90526e4068329616d3618  goblint

Or maybe it is the GCC version or something?

mbs@mbs-VirtualBox:~/Desktop/goblint$ gcc -v
Using built-in specs.
COLLECT_GCC=gcc
COLLECT_LTO_WRAPPER=/usr/lib/gcc/x86_64-linux-gnu/9/lto-wrapper
OFFLOAD_TARGET_NAMES=nvptx-none:hsa
OFFLOAD_TARGET_DEFAULT=1
Target: x86_64-linux-gnu
Configured with: ../src/configure -v --with-pkgversion='Ubuntu 9.2.1-9ubuntu2' --with-bugurl=file:///usr/share/doc/gcc-9/README.Bugs --enable-languages=c,ada,c++,go,brig,d,fortran,objc,obj-c++,gm2 --prefix=/usr --with-gcc-major-version-only --program-suffix=-9 --program-prefix=x86_64-linux-gnu- --enable-shared --enable-linker-build-id --libexecdir=/usr/lib --without-included-gettext --enable-threads=posix --libdir=/usr/lib --enable-nls --enable-bootstrap --enable-clocale=gnu --enable-libstdcxx-debug --enable-libstdcxx-time=yes --with-default-libstdcxx-abi=new --enable-gnu-unique-object --disable-vtable-verify --enable-plugin --enable-default-pie --with-system-zlib --with-target-system-zlib=auto --enable-multiarch --disable-werror --with-arch-32=i686 --with-abi=m64 --with-multilib-list=m32,m64,mx32 --enable-multilib --with-tune=generic --enable-offload-targets=nvptx-none,hsa --without-cuda-driver --enable-checking=release --build=x86_64-linux-gnu --host=x86_64-linux-gnu --target=x86_64-linux-gnu
Thread model: posix
gcc version 9.2.1 20191008 (Ubuntu 9.2.1-9ubuntu2) 

mbs@mbs-VirtualBox:~/Desktop/goblint$ ldd --version
ldd (Ubuntu GLIBC 2.30-0ubuntu2.2) 2.30
Copyright (C) 2019 Free Software Foundation, Inc.
This is free software; see the source for copying conditions.  There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
Written by Roland McGrath and Ulrich Drepper.

mbs@mbs-VirtualBox:~/Desktop/goblint$ lsb_release -a
No LSB modules are available.
Distributor ID:	Ubuntu
Description:	Ubuntu 19.10
Release:	19.10
Codename:	eoan

@sim642
Copy link
Member

sim642 commented Dec 8, 2020

Hmm yeah, it does happen with pals_opt-floodmax.5.2.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c on the archive build, so there is some consistency.

In the supposedly final results (linked in Slack) there's one more case: seq-mthreaded-reduced/pals_opt-floodmax.4.3.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c. It didn't show in the preruns so something weird is even happening there without any change to the archive. And it's nowhere near the timeout.

@michael-schwarz michael-schwarz mentioned this issue Dec 17, 2020
Merged
@jerhard
Copy link
Member

jerhard commented Jun 16, 2021

For the first example at least, var_eq contains an additional equality between {0, main__i2} in what the solver computed, that is not there for the RHS, but he value domain still knows that main__i2 is [0,0].

After merging 0f9f068/ pull #249 this also applies to c/seq-mthreaded-reduced/pals_floodmax.4.1.ufo.UNBOUNDED.pals.c.v+cfa-reducer.c

@michael-schwarz michael-schwarz added this to the SV-COMP 2023 milestone Jul 15, 2022
@sim642 sim642 added the sv-comp SV-COMP (analyses, results), witnesses label Sep 29, 2022
@sim642
Copy link
Member

sim642 commented Sep 29, 2022

Fixed by #809 and #827.

@sim642 sim642 closed this as completed Sep 29, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug sv-comp SV-COMP (analyses, results), witnesses
Projects
None yet
Milestone
SV-COMP 2023
Development

No branches or pull requests
3 participants
@sim642 @jerhard @michael-schwarz