search

goblint / analyzer

Static analysis framework for C
https://goblint.in.tum.de
MIT License
172 stars 72 forks source link

Crash with reluctant incremental analysis on figlet #932

Closed jerhard closed 1 year ago

jerhard commented 1 year ago

Goblint crashes on figlet in with a Not_found exception when running with activated incremental.load and incremental.reluctant.enabled.

The line that causes the exception is a lookup in array_map in Base.

https://github.com/goblint/analyzer/blob/deb6b6776a060269536bf36dbde76638455f5188/src/analyses/base.ml#L114

Stack trace ``` Fatal error: exception Not_found Raised at Stdlib__Hashtbl.MakeSeeded.find in file "hashtbl.ml", line 389, characters 17-32 Called from Goblint_lib__Base.MainFunctor.attributes_varinfo in file "src/analyses/base.ml", line 114, characters 14-45 Called from Goblint_lib__Base.MainFunctor.combine.combine_one in file "src/analyses/base.ml", line 2778, characters 61-114 Called from Goblint_lib__MCP.MCP2.combine.f in file "src/analyses/mCP.ml", line 518, characters 17-69 Called from Goblint_lib__MCP.MCP2.map_deadcode.one_el in file "src/analyses/mCP.ml", line 100, characters 49-78 Called from Stdlib__List.fold_left in file "list.ml", line 121, characters 24-34 Called from Goblint_lib__MCP.MCP2.map_deadcode in file "src/analyses/mCP.ml", line 101, characters 13-35 Called from Goblint_lib__MCP.MCP2.combine in file "src/analyses/mCP.ml", line 520, characters 15-82 Called from Goblint_lib__Constraints.WidenContextLifterSide.lift_fun in file "src/framework/constraints.ml", line 340, characters 25-41 Called from Goblint_lib__Constraints.PathSensitive2.combine.k in file "src/framework/constraints.ml", line 1039, characters 16-56 Called from BatSet.Concrete.fold in file "src/batSet.ml", line 310, characters 35-56 Called from Goblint_lib__Constraints.PathSensitive2.combine in file "src/framework/constraints.ml", line 1046, characters 12-33 Called from Goblint_lib__Constraints.DeadCodeLifter.lift_fun in file "src/framework/constraints.ml", line 410, characters 13-29 Called from Goblint_lib__Constraints.HashconsLifter.combine in file "src/framework/constraints.ml", line 76, characters 14-63 Called from Goblint_lib__Constraints.FromSpec.tf_normal_call.combine in file "src/framework/constraints.ml", line 606, characters 14-63 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.tf_normal_call in file "src/framework/constraints.ml", line 617, characters 16-38 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.tf_proc in file "src/framework/constraints.ml", line 650, characters 17-48 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.fold_left2 in file "src/batList.mlv", line 660, characters 39-54 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.simple_solve in file "src/solvers/td3.ml", line 235, characters 46-59 Called from Goblint_lib__Td3.WP.solve.eval in file "src/solvers/td3.ml", line 263, characters 18-36 Called from BatInnerPervasives.(%) in file "src/batInnerPervasives.mlv", line 77, characters 20-25 Called from Goblint_lib__Constraints.FromSpec.tf in file "src/framework/constraints.ml", line 687, characters 15-25 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28 Called from Goblint_lib__Constraints.FromSpec.system.tf in file "src/framework/constraints.ml", line 723, characters 27-47 Called from Goblint_lib__Constraints.EqConstrSysFromGlobConstrSys.conv in file "src/framework/constraints.ml", line 859, characters 4-105 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from Goblint_lib__Td3.WP.solve.solve in file "src/solvers/td3.ml", line 181, characters 14-39 Called from Goblint_lib__Td3.WP.solve.(fun) in file "src/solvers/td3.ml", line 705, characters 14-27 Called from Stdlib__Hashtbl.iter.do_bucket in file "hashtbl.ml", line 159, characters 8-18 Called from Stdlib__Hashtbl.iter in file "hashtbl.ml", line 165, characters 6-21 Re-raised at Stdlib__Hashtbl.iter in file "hashtbl.ml", line 170, characters 4-13 Called from Goblint_lib__Td3.WP.solve in file "src/solvers/td3.ml", line 703, characters 10-587 Called from Goblint_lib__Td3.WP.solve in file "src/solvers/td3.ml", line 1096, characters 21-41 Called from Goblint_lib__Selector.Make.solve in file "src/solvers/selector.ml", line 28, characters 26-43 Called from Goblint_lib__Constraints.GlobSolverFromEqSolver.solve in file "src/framework/constraints.ml", line 929, characters 30-56 Called from Goblint_timing.Make.wrap in file "src/util/timing/goblint_timing.ml", line 140, characters 10-13 Re-raised at Goblint_timing.Make.wrap in file "src/util/timing/goblint_timing.ml", line 146, characters 6-13 Called from Goblint_lib__Control.AnalyzeCFG.analyze.solve_and_postprocess in file "src/framework/control.ml", line 466, characters 38-114 Called from Goblint_lib__Timeout.Unix.timeout in file "src/util/timeout.ml", line 6, characters 14-19 Called from Goblint_lib__Control.AnalyzeCFG.analyze in file "src/framework/control.ml", line 617, characters 17-100 Called from Goblint_lib__Control.analyze_loop.(fun) in file "src/framework/control.ml", line 694, characters 4-21 Called from Goblint_lib__Maingoblint.do_analyze.control_analyze in file "src/maingoblint.ml", line 461, characters 10-46 Re-raised at Goblint_lib__Maingoblint.do_analyze.control_analyze in file "src/maingoblint.ml", line 470, characters 8-49 Called from Goblint_timing.Make.wrap in file "src/util/timing/goblint_timing.ml", line 140, characters 10-13 Re-raised at Goblint_timing.Make.wrap in file "src/util/timing/goblint_timing.ml", line 146, characters 6-13 Called from Dune__exe__Goblint.main in file "src/goblint.ml", line 62, characters 6-35 Called from Stdlib.at_exit.new_exit in file "stdlib.ml", line 560, characters 59-63 Called from Stdlib.do_at_exit in file "stdlib.ml" (inlined), line 566, characters 20-61 Called from Std_exit in file "std_exit.ml", line 18, characters 8-20 ``` `array_map` may not be correctly initialized in an incremental reluctant run. Interestingly, this issue is not exhibited in a incremental run where reluctant is disabled.
jerhard commented 1 year ago

@michael-schwarz and I looked into this. The issue arises from the fact that array_map is populated in enter with the callee; while in combine the entry for the caller is looked up. In the reluctant runs, the caller is therefore not necessarily in the hashtable, as calls to the caller are not necessarily recomputed.

I will marshal the array_map, so that the mapping from the previous run is preserved.

sim642 commented 1 year ago

I will marshal the array_map, so that the mapping from the previous run is preserved.

The alternative would be putting array_map also into the constraint system, but just marshaling it would be easier for now if it works.