Add support for reading GOTO functions from JSON

doc/man/symtab2gb.1

@@ -19,6 +19,9 @@ https://github.com/model-checking/kani).
 \fB\-\-out\fR \fIoutfile\fR
 Specify the filename of the resulting binary (default: a.out)
 .TP
+\fB\-\-goto\-functions\fR \fIfile\fR
+Specify a file containing JSON-encoded goto functions
+.TP
 \fB\-\-verbosity\fR #
 verbosity level
 .SH ENVIRONMENT

jbmc/regression/jdiff/java-properties/test.desc

@@ -5,6 +5,6 @@ old.jar --json-ui --show-properties --cover location
 activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
-  "deletedFunctions": \[\n      \{\n        "name": "java::Test.obsolete:\(\)V",\n        "properties": \[\n          \{\n            "basicBlockLines": \{\n              "Test.java": \{\n                "java::Test.obsolete:\(\)V": "18"\n              \}\n            \},\n            "class": "coverage",\n            "description": "block 1 \(lines Test.java:java::Test.obsolete:\(\)V:18\)",\n            "expression": "false",\n            "name": "java::Test.obsolete:\(\)V.coverage.1",\n            "sourceLocation": \{\n              "bytecodeIndex": "0",\n              "file": "Test.java",\n              "function": "java::Test.obsolete:\(\)V",\n              "line": "18"\n            }\n          }\n        ],\n        "sourceLocation": \{\n          "file": "Test.java",\n          "function": "java::Test.obsolete:\(\)V",\n          "line": "18"\n        }\n      }\n    ],\n    "modifiedFunctions": \[\n      \{\n        "name": "java::Test.<init>:\(\)V",\n        "properties": \[\n          \{\n            "basicBlockLines": \{\n              "Test.java": \{\n                "java::Test.<init>:\(\)V": "6"\n              \}\n            \},\n            "class": "coverage",\n            "description": "block 2 \(lines Test.java:java::Test.<init>:\(\)V:6\)",\n            "expression": "false",\n            "name": "java::Test.<init>:\(\)V.coverage.1",\n            "sourceLocation": \{\n              "bytecodeIndex": "1",\n              "file": "Test.java",\n              "function": "java::Test.<init>:\(\)V",\n              "line": "6"\n            }\n          },\n          \{\n            "basicBlockLines": \{\n              "Test.java": \{\n                "java::Test.<init>:\(\)V": "4"\n              \}\n            \},\n            "class": "coverage",\n            "description": "block 3 \(lines Test.java:java::Test.<init>:\(\)V:4\)",\n            "expression": "false",\n            "name": "java::Test.<init>:\(\)V.coverage.2",\n            "sourceLocation": \{\n              "bytecodeIndex": "3",\n              "file": "Test.java",\n              "function": "java::Test.<init>:\(\)V",\n              "line": "4"\n            }\n          },\n          \{\n            "basicBlockLines": \{\n              "Test.java": \{\n                "java::Test.<init>:\(\)V": "4"\n              \}\n            \},\n            "class": "coverage",\n            "description": "block 4 \(lines Test.java:java::Test.<init>:\(\)V:4\)",\n            "expression": "false",\n            "name": "java::Test.<init>:\(\)V.coverage.3",\n            "sourceLocation": \{\n              "bytecodeIndex": "5",\n              "file": "Test.java",\n              "function": "java::Test.<init>:\(\)V",\n              "line": "4"\n            }\n          },\n          \{\n            "basicBlockLines": \{\n              "Test.java": \{\n                "java::Test.<init>:\(\)V": "4"\n              \}\n            \},\n            "class": "coverage",\n            "description": "block 5 \(lines Test.java:java::Test.<init>:\(\)V:4\)",\n            "expression": "false",\n            "name": "java::Test.<init>:\(\)V.coverage.4",\n            "sourceLocation": \{\n              "bytecodeIndex": "6",\n              "file": "Test.java",\n              "function": "java::Test.<init>:\(\)V",\n              "line": "4"\n            }\n          },\n          \{\n            "basicBlockLines": \{\n              "Test.java": \{\n                "java::Test.<init>:\(\)V": "7"\n              \}\n            \},\n            "class": "coverage",\n            "description": "block 6 \(lines Test.java:java::Test.<init>:\(\)V:7\)",\n            "expression": "false",\n            "name": "java::Test.<init>:\(\)V.coverage.5",\n            "sourceLocation": \{\n              "bytecodeIndex": "7",\n              "file": "Test.java",\n              "function": "java::Test.<init>:\(\)V",\n              "line": "7"\n            }\n          }\n        ],\n        "sourceLocation": \{\n          "file": "Test.java",\n          "function": "java::Test.<init>:\(\)V",\n          "line": "6"\n        }\n      },\n      \{\n        "name": "java::Test.<clinit>:\(\)V",\n        "properties": \[\n          \{\n            "basicBlockLines": \{\n              "Test.java": \{\n                "java::Test.<clinit>:\(\)V": "3"\n              \}\n            \},\n            "class": "coverage",\n            "description": "block 1 \(lines Test.java:java::Test.<clinit>:\(\)V:3\)",\n            "expression": "false",\n            "name": "java::Test.<clinit>:\(\)V.coverage.1",\n            "sourceLocation": \{\n              "bytecodeIndex": "1",\n              "file": "Test.java",\n              "function": "java::Test.<clinit>:\(\)V",\n              "line": "3"\n            }\n          }\n        ],\n        "sourceLocation": \{\n          "file": "Test.java",\n          "function": "java::Test.<clinit>:\(\)V",\n          "line": "3"\n        }\n      }\n    ],\n    "newFunctions": \[\n      \{\n        "name": "java::Test.newfun:\(\)V",\n        "properties": \[\n          \{\n            "basicBlockLines": \{\n              "Test.java": \{\n                "java::Test.newfun:\(\)V": "18"\n              \}\n            \},\n            "class": "coverage",\n            "description": "block 1 \(lines Test.java:java::Test.newfun:\(\)V:18\)",\n            "expression": "false",\n            "name": "java::Test.newfun:\(\)V.coverage.1",\n            "sourceLocation": \{\n              "bytecodeIndex": "0",\n              "file": "Test.java",\n              "function": "java::Test.newfun:\(\)V",\n              "line": "18"\n            }\n          }\n        ],\n        "sourceLocation": \{\n          "file": "Test.java",\n          "function": "java::Test.newfun:\(\)V",\n          "line": "18"\n        }\n      }\n    ],\n  
+\s*"deletedFunctions": \[\n\s*\{\n\s*"name": "java::Test.obsolete:\(\)V",\n\s*"properties": \[\n\s*\{\n\s*"basicBlockLines": \{\n\s*"Test.java": \{\n\s*"java::Test.obsolete:\(\)V": "18"\n\s*\}\n\s*\},\n\s*"class": "coverage",\n\s*"description": "block 1 \(lines Test.java:java::Test.obsolete:\(\)V:18\)",\n\s*"expression": "false",\n\s*"name": "java::Test.obsolete:\(\)V.coverage.1",\n\s*"sourceLocation": \{\n\s*"basicBlockSourceLines": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"Test.java": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"java::Test.obsolete:\(\)V": \{\n\s*"id": "18"\n\s*\}\n\s*\}\n\s*\}\n\s*\}\n\s*\},\n\s*"bytecodeIndex": "0",\n\s*"comment": "block 1 \(lines Test.java:java::Test.obsolete:\(\)V:18\)",\n\s*"file": "Test.java",\n\s*"function": "java::Test.obsolete:\(\)V",\n\s*"line": "18",\n\s*"propertyClass": "coverage",\n\s*"propertyId": "java::Test.obsolete:\(\)V.coverage.1"\n\s*\}\n\s*\}\n\s*\],\n\s*"sourceLocation": \{\n\s*"file": "Test.java",\n\s*"function": "java::Test.obsolete:\(\)V",\n\s*"line": "18"\n\s*\}\n\s*\}\n\s*\],\n\s*"modifiedFunctions": \[\n\s*\{\n\s*"name": "java::Test.<init>:\(\)V",\n\s*"properties": \[\n\s*\{\n\s*"basicBlockLines": \{\n\s*"Test.java": \{\n\s*"java::Test.<init>:\(\)V": "6"\n\s*\}\n\s*\},\n\s*"class": "coverage",\n\s*"description": "block 2 \(lines Test.java:java::Test.<init>:\(\)V:6\)",\n\s*"expression": "false",\n\s*"name": "java::Test.<init>:\(\)V.coverage.1",\n\s*"sourceLocation": \{\n\s*"basicBlockSourceLines": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"Test.java": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"java::Test.<init>:\(\)V": \{\n\s*"id": "6"\n\s*\}\n\s*\}\n\s*\}\n\s*\}\n\s*\},\n\s*"bytecodeIndex": "1",\n\s*"comment": "block 2 \(lines Test.java:java::Test.<init>:\(\)V:6\)",\n\s*"file": "Test.java",\n\s*"function": "java::Test.<init>:\(\)V",\n\s*"line": "6",\n\s*"propertyClass": "coverage",\n\s*"propertyId": "java::Test.<init>:\(\)V.coverage.1"\n\s*\}\n\s*\},\n\s*\{\n\s*"basicBlockLines": \{\n\s*"Test.java": \{\n\s*"java::Test.<init>:\(\)V": "4"\n\s*\}\n\s*\},\n\s*"class": "coverage",\n\s*"description": "block 3 \(lines Test.java:java::Test.<init>:\(\)V:4\)",\n\s*"expression": "false",\n\s*"name": "java::Test.<init>:\(\)V.coverage.2",\n\s*"sourceLocation": \{\n\s*"basicBlockSourceLines": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"Test.java": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"java::Test.<init>:\(\)V": \{\n\s*"id": "4"\n\s*\}\n\s*\}\n\s*\}\n\s*\}\n\s*\},\n\s*"bytecodeIndex": "3",\n\s*"comment": "block 3 \(lines Test.java:java::Test.<init>:\(\)V:4\)",\n\s*"file": "Test.java",\n\s*"function": "java::Test.<init>:\(\)V",\n\s*"line": "4",\n\s*"propertyClass": "coverage",\n\s*"propertyId": "java::Test.<init>:\(\)V.coverage.2"\n\s*\}\n\s*\},\n\s*\{\n\s*"basicBlockLines": \{\n\s*"Test.java": \{\n\s*"java::Test.<init>:\(\)V": "4"\n\s*\}\n\s*\},\n\s*"class": "coverage",\n\s*"description": "block 4 \(lines Test.java:java::Test.<init>:\(\)V:4\)",\n\s*"expression": "false",\n\s*"name": "java::Test.<init>:\(\)V.coverage.3",\n\s*"sourceLocation": \{\n\s*"basicBlockSourceLines": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"Test.java": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"java::Test.<init>:\(\)V": \{\n\s*"id": "4"\n\s*\}\n\s*\}\n\s*\}\n\s*\}\n\s*\},\n\s*"bytecodeIndex": "5",\n\s*"comment": "block 4 \(lines Test.java:java::Test.<init>:\(\)V:4\)",\n\s*"file": "Test.java",\n\s*"function": "java::Test.<init>:\(\)V",\n\s*"line": "4",\n\s*"propertyClass": "coverage",\n\s*"propertyId": "java::Test.<init>:\(\)V.coverage.3"\n\s*\}\n\s*\},\n\s*\{\n\s*"basicBlockLines": \{\n\s*"Test.java": \{\n\s*"java::Test.<init>:\(\)V": "4"\n\s*\}\n\s*\},\n\s*"class": "coverage",\n\s*"description": "block 5 \(lines Test.java:java::Test.<init>:\(\)V:4\)",\n\s*"expression": "false",\n\s*"name": "java::Test.<init>:\(\)V.coverage.4",\n\s*"sourceLocation": \{\n\s*"basicBlockSourceLines": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"Test.java": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"java::Test.<init>:\(\)V": \{\n\s*"id": "4"\n\s*\}\n\s*\}\n\s*\}\n\s*\}\n\s*\},\n\s*"bytecodeIndex": "6",\n\s*"comment": "block 5 \(lines Test.java:java::Test.<init>:\(\)V:4\)",\n\s*"file": "Test.java",\n\s*"function": "java::Test.<init>:\(\)V",\n\s*"line": "4",\n\s*"propertyClass": "coverage",\n\s*"propertyId": "java::Test.<init>:\(\)V.coverage.4"\n\s*\}\n\s*\},\n\s*\{\n\s*"basicBlockLines": \{\n\s*"Test.java": \{\n\s*"java::Test.<init>:\(\)V": "7"\n\s*\}\n\s*\},\n\s*"class": "coverage",\n\s*"description": "block 6 \(lines Test.java:java::Test.<init>:\(\)V:7\)",\n\s*"expression": "false",\n\s*"name": "java::Test.<init>:\(\)V.coverage.5",\n\s*"sourceLocation": \{\n\s*"basicBlockSourceLines": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"Test.java": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"java::Test.<init>:\(\)V": \{\n\s*"id": "7"\n\s*\}\n\s*\}\n\s*\}\n\s*\}\n\s*\},\n\s*"bytecodeIndex": "7",\n\s*"comment": "block 6 \(lines Test.java:java::Test.<init>:\(\)V:7\)",\n\s*"file": "Test.java",\n\s*"function": "java::Test.<init>:\(\)V",\n\s*"line": "7",\n\s*"propertyClass": "coverage",\n\s*"propertyId": "java::Test.<init>:\(\)V.coverage.5"\n\s*\}\n\s*\}\n\s*\],\n\s*"sourceLocation": \{\n\s*"file": "Test.java",\n\s*"function": "java::Test.<init>:\(\)V",\n\s*"line": "6"\n\s*\}\n\s*\},\n\s*\{\n\s*"name": "java::Test.<clinit>:\(\)V",\n\s*"properties": \[\n\s*\{\n\s*"basicBlockLines": \{\n\s*"Test.java": \{\n\s*"java::Test.<clinit>:\(\)V": "3"\n\s*\}\n\s*\},\n\s*"class": "coverage",\n\s*"description": "block 1 \(lines Test.java:java::Test.<clinit>:\(\)V:3\)",\n\s*"expression": "false",\n\s*"name": "java::Test.<clinit>:\(\)V.coverage.1",\n\s*"sourceLocation": \{\n\s*"basicBlockSourceLines": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"Test.java": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"java::Test.<clinit>:\(\)V": \{\n\s*"id": "3"\n\s*\}\n\s*\}\n\s*\}\n\s*\}\n\s*\},\n\s*"bytecodeIndex": "1",\n\s*"comment": "block 1 \(lines Test.java:java::Test.<clinit>:\(\)V:3\)",\n\s*"file": "Test.java",\n\s*"function": "java::Test.<clinit>:\(\)V",\n\s*"line": "3",\n\s*"propertyClass": "coverage",\n\s*"propertyId": "java::Test.<clinit>:\(\)V.coverage.1"\n\s*\}\n\s*\}\n\s*\],\n\s*"sourceLocation": \{\n\s*"file": "Test.java",\n\s*"function": "java::Test.<clinit>:\(\)V",\n\s*"line": "3"\n\s*\}\n\s*\}\n\s*\],\n\s*"newFunctions": \[\n\s*\{\n\s*"name": "java::Test.newfun:\(\)V",\n\s*"properties": \[\n\s*\{\n\s*"basicBlockLines": \{\n\s*"Test.java": \{\n\s*"java::Test.newfun:\(\)V": "18"\n\s*\}\n\s*\},\n\s*"class": "coverage",\n\s*"description": "block 1 \(lines Test.java:java::Test.newfun:\(\)V:18\)",\n\s*"expression": "false",\n\s*"name": "java::Test.newfun:\(\)V.coverage.1",\n\s*"sourceLocation": \{\n\s*"basicBlockSourceLines": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"Test.java": \{\n\s*"id": "",\n\s*"namedSub": \{\n\s*"java::Test.newfun:\(\)V": \{\n\s*"id": "18"\n\s*\}\n\s*\}\n\s*\}\n\s*\}\n\s*\},\n\s*"bytecodeIndex": "0",\n\s*"comment": "block 1 \(lines Test.java:java::Test.newfun:\(\)V:18\)",\n\s*"file": "Test.java",\n\s*"function": "java::Test.newfun:\(\)V",\n\s*"line": "18",\n\s*"propertyClass": "coverage",\n\s*"propertyId": "java::Test.newfun:\(\)V.coverage.1"\n\s*\}\n\s*\}\n\s*\],\n\s*"sourceLocation": \{\n\s*"file": "Test.java",\n\s*"function": "java::Test.newfun:\(\)V",\n\s*"line": "18"\n\s*\}\n\s*\}\n\s*\],\n
 --
 ^warning: ignoring

regression/CMakeLists.txt

@@ -80,7 +80,6 @@ add_subdirectory(goto-cc-multi-file)
 add_subdirectory(goto-cc-regression-gh-issue-5380)
 add_subdirectory(linking-goto-binaries)
 add_subdirectory(symtab2gb)
-add_subdirectory(symtab2gb-cbmc)
 add_subdirectory(solver-hardness)
 if(NOT WIN32)
   add_subdirectory(goto-ld)

regression/Makefile

@@ -53,7 +53,6 @@ DIRS = cbmc-shadow-memory \
        goto-cc-regression-gh-issue-5380 \
        linking-goto-binaries \
        symtab2gb \
-       symtab2gb-cbmc \
        solver-hardness \
        goto-ld \
        validate-trace-xml-schema \

regression/cbmc-cover/json-goals1/test.desc

@@ -4,6 +4,6 @@ main.c
 activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
-\{\n\s*"goals": \[\n\s*\{\n\s*"basicBlockLines": \{\n\s*"main.c": \{\n\s*"main": "\d+"\n\s*\}\n\s*\},\n\s*"description": "block \d+ \(lines main.c:main:\d+\)",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){5}\},\n\s*"status": "satisfied"\n\s*\},\n\s*\{\n\s*"basicBlockLines": \{\n\s*"main.c": \{\n\s*"main": "\d+"\n\s*\}\n\s*\},\n\s*"description": "block \d+ \(lines main.c:main:\d+\)",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){5}\},\n\s*"status": "satisfied"\n\s*\},\n\s*\{\n\s*"basicBlockLines": \{\n\s*"main.c": \{\n\s*"main": "\d+"\n\s*\}\n\s*\},\n\s*"description": "block \d+ \(lines main.c:main:\d+\)",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){5}\},\n\s*"status": "satisfied"\n\s*\},\n\s*\{\n\s*"basicBlockLines": \{\n\s*"main.c": \{\n\s*"main": "\d+"\n\s*\}\n\s*\},\n\s*"description": "block \d+ \(lines main.c:main:\d+\)",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){5}\},\n\s*"status": "satisfied"\n\s*\}\n\s*\],\n\s*"goalsCovered": 4,\n\s*"totalGoals": 4\n\s*\}
+\{\n\s*"goals": \[\n\s*\{\n\s*"basicBlockLines": \{\n\s*"main.c": \{\n\s*"main": "\d+"\n\s*\}\n\s*\},\n\s*"description": "block \d+ \(lines main.c:main:\d+\)",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){22}\},\n\s*"status": "satisfied"\n\s*\},\n\s*\{\n\s*"basicBlockLines": \{\n\s*"main.c": \{\n\s*"main": "\d+"\n\s*\}\n\s*\},\n\s*"description": "block \d+ \(lines main.c:main:\d+\)",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){22}\},\n\s*"status": "satisfied"\n\s*\},\n\s*\{\n\s*"basicBlockLines": \{\n\s*"main.c": \{\n\s*"main": "\d+"\n\s*\}\n\s*\},\n\s*"description": "block \d+ \(lines main.c:main:\d+\)",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){22}\},\n\s*"status": "satisfied"\n\s*\},\n\s*\{\n\s*"basicBlockLines": \{\n\s*"main.c": \{\n\s*"main": "\d+"\n\s*\}\n\s*\},\n\s*"description": "block \d+ \(lines main.c:main:\d+\)",\n\s*"goal": "main\.coverage\.[1-4]",\n\s*"sourceLocation": \{(\n.+){22}\},\n\s*"status": "satisfied"\n\s*\}\n\s*\],\n\s*"goalsCovered": 4,\n\s*"totalGoals": 4\n\s*\}
 --
 ^warning: ignoring

regression/cbmc/json-interface1/test.desc

@@ -5,8 +5,8 @@ activate-multi-line-match
 ^EXIT=10$
 ^SIGNAL=0$
 Not unwinding loop foo\.0 iteration 3 file main\.c line 5 function foo thread 0
-\{\n\s*"description": "assertion 0",\n\s*"property": "foo\.assertion\.(1|3)",\n\s*"sourceLocation": \{\n\s*"file": "main.c",\n\s*"function": "foo",\n\s*"line": "(8|11)",\n\s*"workingDirectory": ".*json-interface1"\n\s*\},\n\s*"status": "SUCCESS"\n\s*\}
-\{\n\s*"description": "assertion 0",\n\s*"property": "foo\.assertion\.(1|3)",\n\s*"sourceLocation": \{\n\s*"file": "main.c",\n\s*"function": "foo",\n\s*"line": "(8|11)",\n\s*"workingDirectory": ".*json-interface1"\n\s*\},\n\s*"status": "FAILURE",\n\s*"trace": \[
+\{\n\s*"description": "assertion 0",\n\s*"property": "foo\.assertion\.(1|3)",\n\s*"sourceLocation": \{\n\s*"comment": "assertion 0",\n\s*"file": "main.c",\n\s*"function": "foo",\n\s*"line": "(8|11)",\n\s*"pragma":.*\n\s*"propertyClass": "assertion",\n\s*"propertyId": "foo.assertion.\d+",\n\s*"workingDirectory": ".*json-interface1"\n\s*\},\n\s*"status": "SUCCESS"\n\s*\}
+\{\n\s*"description": "assertion 0",\n\s*"property": "foo\.assertion\.(1|3)",\n\s*"sourceLocation": \{\n\s*"comment": "assertion 0",\n\s*"file": "main.c",\n\s*"function": "foo",\n\s*"line": "(8|11)",\n\s*"pragma":.*\n\s*"propertyClass": "assertion",\n\s*"propertyId": "foo.assertion.\d+",\n\s*"workingDirectory": ".*json-interface1"\n\s*\},\n\s*"status": "FAILURE",\n\s*"trace": \[
 VERIFICATION FAILED
 --
 "property": "foo\.assertion\.2"

regression/cbmc/loophead-trace/test-json.desc

@@ -4,7 +4,7 @@ test.c
 activate-multi-line-match
 ^EXIT=10$
 ^SIGNAL=0$
-\s*\{\n\s*  .*\n\s*  "sourceLocation": \{\n\s*    .*,\n\s*    .*,\n\s*    "line": "5",\n\s*    .*\n\s*  \},\n\s*  "stepType": "loop-head",\n\s*  .*\n\s*\},\n\s*\{\n\s*  .*\n\s*  "sourceLocation": \{\n\s*    .*,\n\s*    .*,\n\s*    "line": "5",\n\s*    .*\n\s*  \},\n\s*  "stepType": "loop-head",\n\s*  .*\n\s*\},
+\s*\{\n\s*  .*\n\s*  "sourceLocation": \{\n\s*    .*,\n\s*    .*,\n\s*    "line": "5",\n\s*    .*,\n\s*    .*\n\s*  \},\n\s*  "stepType": "loop-head",\n\s*  .*\n\s*\},\n\s*\{\n\s*  .*\n\s*  "sourceLocation": \{\n\s*    .*,\n\s*    .*,\n\s*    "line": "5",\n\s*    .*,\n\s*    .*\n\s*  \},\n\s*  "stepType": "loop-head",\n\s*  .*\n\s*\},
 --
 --
 Ensure even with sliced formulas, we get a location only step for

regression/solver-hardness/guards/test.desc

@@ -5,9 +5,9 @@ main.c
 ^SIGNAL=0$
 ^\[main.assertion.1\] line 12 should fail: FAILURE$
 ^VERIFICATION FAILED$
-\{"GOTO":"GOTO \d+","GOTO_ID":\d+,"SAT_hardness":\{"ClauseSet":\[\d+.*\],"Clauses":[1-9]\d*,"Literals":[1-9]\d*,"Variables":[1-9]\d*},"SSA_expr":"goto_symex::\\\\guard#1 ∧ goto_symex::\\\\guard#2","Source":\{"file":"main.c","function":"main","line":"\d+","workingDirectory":".*"\}\}
+\{"GOTO":"GOTO \d+","GOTO_ID":\d+,"SAT_hardness":\{"ClauseSet":\[\d+.*\],"Clauses":[1-9]\d*,"Literals":[1-9]\d*,"Variables":[1-9]\d*},"SSA_expr":"goto_symex::\\\\guard#1 ∧ goto_symex::\\\\guard#2","Source":\{"file":"main.c","function":"main","line":"\d+","pragma":.*,"propertyClass":.*,"propertyId":.*,"workingDirectory":".*"\}\}
 --
 ^warning: ignoring
-\{"GOTO":"GOTO \d+","GOTO_ID":\d+,"SAT_hardness":\{"ClauseSet":\[\d+.*\],"Clauses":[1-9]\d*,"Literals":[1-9]\d*,"Variables":[1-9]\d*},"SSA_expr":"true","Source":\{"file":"main.c","function":"main","line":"\d+","workingDirectory":".*"\}\}
+\{"GOTO":"GOTO \d+","GOTO_ID":\d+,"SAT_hardness":\{"ClauseSet":\[\d+.*\],"Clauses":[1-9]\d*,"Literals":[1-9]\d*,"Variables":[1-9]\d*},"SSA_expr":"true","Source":\{"file":"main.c","function":"main","line":"\d+","pragma":.*,"propertyClass":.*,"propertyId":.*,"workingDirectory":".*"\}\}
 --
 "true" must not yield any clauses.