./Dartagnan-SVCOMP.sh /mnt/goblint-svcomp/goblint-bench/bench/concrat/properties/no-data-race.prp /mnt/goblint-svcomp/goblint-bench/bench/concrat/the_silver_searcher/main.c


--------------------------------------------------------------------------------


02:25:15 [INFO ] GitInfo.CreateGitInfo - Git branch: svcomp-2024
02:25:15 [INFO ] GitInfo.CreateGitInfo - Git commit ID: 17eeec33cbc9c310519b08551b317469f878ce8c
02:25:15 [INFO ] GlobalSettings.LogGlobalSettings - REFINEMENT_GENERATE_GRAPHVIZ_DEBUG_FILES: false
02:25:15 [INFO ] GlobalSettings.LogGlobalSettings - REFINEMENT_SYMMETRIC_LEARNING: FULL
02:25:15 [INFO ] Dartagnan.main - Program path: /mnt/goblint-svcomp/benchexec/tools-pldi24/dartagnan/output/main-opt.ll
02:25:15 [INFO ] Dartagnan.main - CAT file path: cat/svcomp.cat
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv32. Constant was replaced by zero.
02:25:16 [WARN ] VisitorLlvm.visitUndefConst - Encountered undef constant of type bv64. Constant was replaced by zero.
Exception in thread "main" java.lang.UnsupportedOperationException: Parsing of instruction %249=sitofpi64%248todouble.
	at com.dat3m.dartagnan.parsers.program.visitors.VisitorLlvm.visitLocalDefInst(VisitorLlvm.java:462)
	at com.dat3m.dartagnan.parsers.program.visitors.VisitorLlvm.visitLocalDefInst(VisitorLlvm.java:39)
	at com.dat3m.dartagnan.parsers.LLVMIRParser$LocalDefInstContext.accept(LLVMIRParser.java:12201)
	at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
	at com.dat3m.dartagnan.parsers.LLVMIRBaseVisitor.visitInstruction(LLVMIRBaseVisitor.java:231)
	at com.dat3m.dartagnan.parsers.LLVMIRParser$InstructionContext.accept(LLVMIRParser.java:3166)
	at com.dat3m.dartagnan.parsers.program.visitors.VisitorLlvm.parseBlockInstructionWithMetadata(VisitorLlvm.java:220)
	at com.dat3m.dartagnan.parsers.program.visitors.VisitorLlvm.visitFuncDef(VisitorLlvm.java:179)
	at com.dat3m.dartagnan.parsers.program.visitors.VisitorLlvm.visitFuncDef(VisitorLlvm.java:39)
	at com.dat3m.dartagnan.parsers.LLVMIRParser$FuncDefContext.accept(LLVMIRParser.java:1663)
	at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
	at com.dat3m.dartagnan.parsers.LLVMIRBaseVisitor.visitTopLevelEntity(LLVMIRBaseVisitor.java:56)
	at com.dat3m.dartagnan.parsers.LLVMIRParser$TopLevelEntityContext.accept(LLVMIRParser.java:840)
	at com.dat3m.dartagnan.parsers.program.visitors.VisitorLlvm.visitCompilationUnit(VisitorLlvm.java:113)
	at com.dat3m.dartagnan.parsers.program.visitors.VisitorLlvm.visitCompilationUnit(VisitorLlvm.java:39)
	at com.dat3m.dartagnan.parsers.LLVMIRParser$CompilationUnitContext.accept(LLVMIRParser.java:535)
	at com.dat3m.dartagnan.parsers.program.ParserLlvm.parse(ParserLlvm.java:22)
	at com.dat3m.dartagnan.parsers.program.ProgramParser.parse(ProgramParser.java:35)
	at com.dat3m.dartagnan.Dartagnan.main(Dartagnan.java:105)
