Merge pull request #13586 from GeorgePlotnikov/use-pretty-json-for-cmlinetests-output

Use `--pretty-json` for `cmdlineTests.sh` output by default

ReviewChecklist.md

@@ -26,6 +26,13 @@ It is also meant to serve as a final checklist for reviewers to go through befor
     - [ ] Avoid basing PRs from forks on branches other than `develop` or `breaking` because
         GitHub closes them when the base branch gets merged.
         Do this only for PRs created directly in the main repo.
+- [ ] **Does the PR update test expectations to match the modified code?** If not, your PR will not pass some of the `_soltest_`,  jobs in CI.
+    In many cases the expectations can be updated automatically:
+    - `cmdlineTests.sh --update` for command-line tests.
+    - `isoltest --enforce-gas-cost --accept-updates` for soltest-based tests.
+        - If your PR affects gas costs, an extra run of `isoltest --enforce-gas-cost --optimize --accept-updates` is needed to update gas expectations with optimizer enabled.
+    - Review updated files before committing them.
+        **Are expectations correct and do updated tests still serve their purpose?**
 
 ## Coding Style and Good Practices
 - [ ] Does the PR follow our [coding style](CODING_STYLE.md)?
@@ -127,8 +134,6 @@ The following points are all covered by the coding style but come up so often th
 - [ ] **Do not include version pragma and the SPDX comment in semantic and syntax test cases**.
     In other test types include them if necessary to suppress warnings.
 - [ ] **If you have to use a version pragma, avoid hard-coding version.** Use `pragma solidity *`.
-- [ ] **Add `--pretty-print --pretty-json 4` to the `args` file of in command-line tests** to get
-    readable, indented output.
 - [ ] **When writing StandardJSON command-line tests, use `urls` instead of `content`** and put
     the Solidity or Yul code in a separate file.
 

test/cmdlineTests.sh

@@ -186,25 +186,25 @@ function test_solc_behaviour
     exitCode=$?
     set -e
 
-    if [[ " ${solc_args[*]} " == *" --standard-json "* ]]
+    if [[ " ${solc_args[*]} " == *" --standard-json "* ]] && [[ -s $stdout_path ]]
     then
         python3 - <<EOF
 import re, sys
 json = open("$stdout_path", "r").read()
 json = re.sub(r"{[^{}]*Warning: This is a pre-release compiler version[^{}]*},?", "", json)
-json = re.sub(r"\"errors\":\s*\[\s*\],?\s*","",json)    # Remove "errors" array if it's not empty
+json = re.sub(r"\"errors\":\s*\[\s*\],?","\n" if json[1] == " " else "",json)       # Remove "errors" array if it's not empty
-json = re.sub("\n\\s+\n", "\n\n", json)                 # Remove trailing whitespace
+json = re.sub("\n\\s*\n", "\n", json)                                               # Remove trailing whitespace
-json = re.sub(r"},(\n{0,1})\n*(\s*])", r"}\1\2", json)  # },] -> }]
+json = re.sub(r"},(\n{0,1})\n*(\s*(]|}))", r"}\1\2", json)                          # Remove trailing comma
 open("$stdout_path", "w").write(json)
 EOF
         sed -i.bak -E -e 's/ Consider adding \\"pragma solidity \^[0-9.]*;\\"//g' "$stdout_path"
-        sed -i.bak -E -e 's/\"opcodes\":\"[^"]+\"/\"opcodes\":\"<OPCODES REMOVED>\"/g' "$stdout_path"
+        sed -i.bak -E -e 's/\"opcodes\":[[:space:]]*\"[^"]+\"/\"opcodes\":\"<OPCODES REMOVED>\"/g' "$stdout_path"
-        sed -i.bak -E -e 's/\"sourceMap\":\"[0-9:;-]+\"/\"sourceMap\":\"<SOURCEMAP REMOVED>\"/g' "$stdout_path"
+        sed -i.bak -E -e 's/\"sourceMap\":[[:space:]]*\"[0-9:;-]+\"/\"sourceMap\":\"<SOURCEMAP REMOVED>\"/g' "$stdout_path"
 
         # Remove bytecode (but not linker references).
-        sed -i.bak -E -e 's/(\"object\":\")[0-9a-f]+([^"]*\")/\1<BYTECODE REMOVED>\2/g' "$stdout_path"
+        sed -i.bak -E -e 's/(\"object\":[[:space:]]*\")[0-9a-f]+([^"]*\")/\1<BYTECODE REMOVED>\2/g' "$stdout_path"
         # shellcheck disable=SC2016
-        sed -i.bak -E -e 's/(\"object\":\"[^"]+\$__)[0-9a-f]+(\")/\1<BYTECODE REMOVED>\2/g' "$stdout_path"
+        sed -i.bak -E -e 's/(\"object\":[[:space:]]*\"[^"]+\$__)[0-9a-f]+(\")/\1<BYTECODE REMOVED>\2/g' "$stdout_path"
         # shellcheck disable=SC2016
         sed -i.bak -E -e 's/([0-9a-f]{34}\$__)[0-9a-f]+(__\$[0-9a-f]{17})/\1<BYTECODE REMOVED>\2/g' "$stdout_path"
         # Remove metadata in assembly output (see below about the magic numbers)
@@ -215,7 +215,7 @@ EOF
         # Replace escaped newlines by actual newlines for readability
         # shellcheck disable=SC1003
         sed -i.bak -E -e 's/\\n/\'$'\n/g' "$stdout_path"
-        sed -i.bak -e 's/\(^[ ]*auxdata: \)0x[0-9a-f]*$/\1<AUXDATA REMOVED>/' "$stdout_path"
+        sed -i.bak -e 's/\(^[ ]*auxdata:[[:space:]]\)0x[0-9a-f]*$/\1<AUXDATA REMOVED>/' "$stdout_path"
         rm "$stdout_path.bak"
     else
         sed -i.bak -e '/^Warning: This is a pre-release compiler version, please do not use it in production./d' "$stderr_path"
@@ -458,7 +458,13 @@ printTask "Running general commandline tests..."
             inputFile=""
             stdout="$(cat "${tdir}/output.json" 2>/dev/null || true)"
             stdoutExpectationFile="${tdir}/output.json"
-            command_args="--standard-json "$(cat "${tdir}/args" 2>/dev/null || true)
+            prettyPrintFlags=""
+            if [[ ! -f "${tdir}/no-pretty-print" ]]
+            then
+                prettyPrintFlags="--pretty-json --json-indent 4"
+            fi
+
+            command_args="--standard-json ${prettyPrintFlags} "$(cat "${tdir}/args" 2>/dev/null || true)
         else
             if [ -e "${tdir}/stdin" ]
             then

test/cmdlineTests/linking_standard_solidity/output.json

@@ -1 +1,26 @@
-{"contracts":{"A":{"C":{"evm":{"bytecode":{"linkReferences":{},"object":"<BYTECODE REMOVED>"}}}}},"sources":{"A":{"id":0}}}
+{
+    "contracts":
+    {
+        "A":
+        {
+            "C":
+            {
+                "evm":
+                {
+                    "bytecode":
+                    {
+                        "linkReferences": {},
+                        "object": "<BYTECODE REMOVED>"
+                    }
+                }
+            }
+        }
+    },
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/linking_standard_solidity_quote_in_file_name/output.json

@@ -1 +1,26 @@
-{"contracts":{"A\"B":{"C":{"evm":{"bytecode":{"linkReferences":{},"object":"<BYTECODE REMOVED>"}}}}},"sources":{"A\"B":{"id":0}}}
+{
+    "contracts":
+    {
+        "A\"B":
+        {
+            "C":
+            {
+                "evm":
+                {
+                    "bytecode":
+                    {
+                        "linkReferences": {},
+                        "object": "<BYTECODE REMOVED>"
+                    }
+                }
+            }
+        }
+    },
+    "sources":
+    {
+        "A\"B":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/linking_standard_solidity_unresolved_references/output.json

@@ -1 +1,42 @@
-{"contracts":{"A":{"C":{"evm":{"bytecode":{"linkReferences":{"A":{"L2":[{"length":20,"start":184},{"length":20,"start":368}]}},"object":"<BYTECODE REMOVED>__$622b2f540b6a16ff5db7bea656ad8fcf4f$__<BYTECODE REMOVED>__$622b2f540b6a16ff5db7bea656ad8fcf4f$__<BYTECODE REMOVED>"}}}}},"sources":{"A":{"id":0}}}
+{
+    "contracts":
+    {
+        "A":
+        {
+            "C":
+            {
+                "evm":
+                {
+                    "bytecode":
+                    {
+                        "linkReferences":
+                        {
+                            "A":
+                            {
+                                "L2":
+                                [
+                                    {
+                                        "length": 20,
+                                        "start": 184
+                                    },
+                                    {
+                                        "length": 20,
+                                        "start": 368
+                                    }
+                                ]
+                            }
+                        },
+                        "object": "<BYTECODE REMOVED>__$622b2f540b6a16ff5db7bea656ad8fcf4f$__<BYTECODE REMOVED>__$622b2f540b6a16ff5db7bea656ad8fcf4f$__<BYTECODE REMOVED>"
+                    }
+                }
+            }
+        }
+    },
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/linking_standard_yul/output.json

@@ -1 +1,19 @@
-{"contracts":{"A":{"a":{"evm":{"bytecode":{"linkReferences":{},"object":"<BYTECODE REMOVED>"}}}}},}
+{
+    "contracts":
+    {
+        "A":
+        {
+            "a":
+            {
+                "evm":
+                {
+                    "bytecode":
+                    {
+                        "linkReferences": {},
+                        "object": "<BYTECODE REMOVED>"
+                    }
+                }
+            }
+        }
+    }
+}

test/cmdlineTests/linking_standard_yul_quote_in_file_name/output.json

@@ -1 +1,19 @@
-{"contracts":{"A":{"a":{"evm":{"bytecode":{"linkReferences":{},"object":"<BYTECODE REMOVED>"}}}}},}
+{
+    "contracts":
+    {
+        "A":
+        {
+            "a":
+            {
+                "evm":
+                {
+                    "bytecode":
+                    {
+                        "linkReferences": {},
+                        "object": "<BYTECODE REMOVED>"
+                    }
+                }
+            }
+        }
+    }
+}

test/cmdlineTests/linking_standard_yul_unresolved_references/output.json

@@ -1 +1,31 @@
-{"contracts":{"A":{"a":{"evm":{"bytecode":{"linkReferences":{"contract/test.sol":{"L2":[{"length":20,"start":22}]}},"object":"<BYTECODE REMOVED>__$fb58009a6b1ecea3b9d99bedd645df4ec3$__<BYTECODE REMOVED>"}}}}},}
+{
+    "contracts":
+    {
+        "A":
+        {
+            "a":
+            {
+                "evm":
+                {
+                    "bytecode":
+                    {
+                        "linkReferences":
+                        {
+                            "contract/test.sol":
+                            {
+                                "L2":
+                                [
+                                    {
+                                        "length": 20,
+                                        "start": 22
+                                    }
+                                ]
+                            }
+                        },
+                        "object": "<BYTECODE REMOVED>__$fb58009a6b1ecea3b9d99bedd645df4ec3$__<BYTECODE REMOVED>"
+                    }
+                }
+            }
+        }
+    }
+}

test/cmdlineTests/output_selection_all_A1/output.json

@@ -1 +1,42 @@
-{"contracts":{"a.sol":{"A1":{"evm":{"bytecode":{"object":"<BYTECODE REMOVED>"}}}},"b.sol":{"A1":{"evm":{"bytecode":{"object":"<BYTECODE REMOVED>"}}}}},"sources":{"a.sol":{"id":0},"b.sol":{"id":1}}}
+{
+    "contracts":
+    {
+        "a.sol":
+        {
+            "A1":
+            {
+                "evm":
+                {
+                    "bytecode":
+                    {
+                        "object": "<BYTECODE REMOVED>"
+                    }
+                }
+            }
+        },
+        "b.sol":
+        {
+            "A1":
+            {
+                "evm":
+                {
+                    "bytecode":
+                    {
+                        "object": "<BYTECODE REMOVED>"
+                    }
+                }
+            }
+        }
+    },
+    "sources":
+    {
+        "a.sol":
+        {
+            "id": 0
+        },
+        "b.sol":
+        {
+            "id": 1
+        }
+    }
+}

test/cmdlineTests/output_selection_all_A2/output.json

@@ -1 +1,29 @@
-{"contracts":{"a.sol":{"A2":{"evm":{"bytecode":{"object":"<BYTECODE REMOVED>"}}}}},"sources":{"a.sol":{"id":0},"b.sol":{"id":1}}}
+{
+    "contracts":
+    {
+        "a.sol":
+        {
+            "A2":
+            {
+                "evm":
+                {
+                    "bytecode":
+                    {
+                        "object": "<BYTECODE REMOVED>"
+                    }
+                }
+            }
+        }
+    },
+    "sources":
+    {
+        "a.sol":
+        {
+            "id": 0
+        },
+        "b.sol":
+        {
+            "id": 1
+        }
+    }
+}

test/cmdlineTests/output_selection_all_blank/output.json

@@ -1 +1,13 @@
-{"sources":{"a.sol":{"id":0},"b.sol":{"id":1}}}
+{
+    "sources":
+    {
+        "a.sol":
+        {
+            "id": 0
+        },
+        "b.sol":
+        {
+            "id": 1
+        }
+    }
+}

test/cmdlineTests/output_selection_all_star/output.json

@@ -1 +1,62 @@
-{"contracts":{"a.sol":{"A1":{"evm":{"bytecode":{"object":"<BYTECODE REMOVED>"}}},"A2":{"evm":{"bytecode":{"object":"<BYTECODE REMOVED>"}}}},"b.sol":{"A1":{"evm":{"bytecode":{"object":"<BYTECODE REMOVED>"}}},"B2":{"evm":{"bytecode":{"object":"<BYTECODE REMOVED>"}}}}},"sources":{"a.sol":{"id":0},"b.sol":{"id":1}}}
+{
+    "contracts":
+    {
+        "a.sol":
+        {
+            "A1":
+            {
+                "evm":
+                {
+                    "bytecode":
+                    {
+                        "object": "<BYTECODE REMOVED>"
+                    }
+                }
+            },
+            "A2":
+            {
+                "evm":
+                {
+                    "bytecode":
+                    {
+                        "object": "<BYTECODE REMOVED>"
+                    }
+                }
+            }
+        },
+        "b.sol":
+        {
+            "A1":
+            {
+                "evm":
+                {
+                    "bytecode":
+                    {
+                        "object": "<BYTECODE REMOVED>"
+                    }
+                }
+            },
+            "B2":
+            {
+                "evm":
+                {
+                    "bytecode":
+                    {
+                        "object": "<BYTECODE REMOVED>"
+                    }
+                }
+            }
+        }
+    },
+    "sources":
+    {
+        "a.sol":
+        {
+            "id": 0
+        },
+        "b.sol":
+        {
+            "id": 1
+        }
+    }
+}

test/cmdlineTests/output_selection_single_A1/output.json

@@ -1 +1,29 @@
-{"contracts":{"a.sol":{"A1":{"evm":{"bytecode":{"object":"<BYTECODE REMOVED>"}}}}},"sources":{"a.sol":{"id":0},"b.sol":{"id":1}}}
+{
+    "contracts":
+    {
+        "a.sol":
+        {
+            "A1":
+            {
+                "evm":
+                {
+                    "bytecode":
+                    {
+                        "object": "<BYTECODE REMOVED>"
+                    }
+                }
+            }
+        }
+    },
+    "sources":
+    {
+        "a.sol":
+        {
+            "id": 0
+        },
+        "b.sol":
+        {
+            "id": 1
+        }
+    }
+}

test/cmdlineTests/output_selection_single_B1/output.json

@@ -1 +1,29 @@
-{"contracts":{"b.sol":{"B2":{"evm":{"bytecode":{"object":"<BYTECODE REMOVED>"}}}}},"sources":{"a.sol":{"id":0},"b.sol":{"id":1}}}
+{
+    "contracts":
+    {
+        "b.sol":
+        {
+            "B2":
+            {
+                "evm":
+                {
+                    "bytecode":
+                    {
+                        "object": "<BYTECODE REMOVED>"
+                    }
+                }
+            }
+        }
+    },
+    "sources":
+    {
+        "a.sol":
+        {
+            "id": 0
+        },
+        "b.sol":
+        {
+            "id": 1
+        }
+    }
+}

test/cmdlineTests/output_selection_single_all/output.json

@@ -1 +1,39 @@
-{"contracts":{"a.sol":{"A1":{"evm":{"bytecode":{"object":"<BYTECODE REMOVED>"}}},"A2":{"evm":{"bytecode":{"object":"<BYTECODE REMOVED>"}}}}},"sources":{"a.sol":{"id":0},"b.sol":{"id":1}}}
+{
+    "contracts":
+    {
+        "a.sol":
+        {
+            "A1":
+            {
+                "evm":
+                {
+                    "bytecode":
+                    {
+                        "object": "<BYTECODE REMOVED>"
+                    }
+                }
+            },
+            "A2":
+            {
+                "evm":
+                {
+                    "bytecode":
+                    {
+                        "object": "<BYTECODE REMOVED>"
+                    }
+                }
+            }
+        }
+    },
+    "sources":
+    {
+        "a.sol":
+        {
+            "id": 0
+        },
+        "b.sol":
+        {
+            "id": 1
+        }
+    }
+}

test/cmdlineTests/recovery_standard_json/output.json

@@ -1,13 +1,101 @@
-{"errors":[{"component":"general","errorCode":"3546","formattedMessage":"ParserError: Expected type name
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "3546",
+            "formattedMessage": "ParserError: Expected type name
  --> A:2:58:
   |
 2 | pragma solidity >=0.0; contract Errort6 { using foo for  ; /* missing type name */ }
   |                                                          ^
 
-","message":"Expected type name","severity":"error","sourceLocation":{"end":94,"file":"A","start":93},"type":"ParserError"},{"component":"general","errorCode":"3796","formattedMessage":"Warning: Recovered in ContractDefinition at '}'.
+",
+            "message": "Expected type name",
+            "severity": "error",
+            "sourceLocation":
+            {
+                "end": 94,
+                "file": "A",
+                "start": 93
+            },
+            "type": "ParserError"
+        },
+        {
+            "component": "general",
+            "errorCode": "3796",
+            "formattedMessage": "Warning: Recovered in ContractDefinition at '}'.
  --> A:2:84:
   |
 2 | pragma solidity >=0.0; contract Errort6 { using foo for  ; /* missing type name */ }
   |                                                                                    ^
 
-","message":"Recovered in ContractDefinition at '}'.","severity":"warning","sourceLocation":{"end":120,"file":"A","start":119},"type":"Warning"}],"sources":{"A":{"ast":{"absolutePath":"A","exportedSymbols":{"Errort6":[3]},"id":4,"license":"GPL-3.0","nodeType":"SourceUnit","nodes":[{"id":1,"literals":["solidity",">=","0.0"],"nodeType":"PragmaDirective","src":"36:22:0"},{"abstract":false,"baseContracts":[],"canonicalName":"Errort6","contractDependencies":[],"contractKind":"contract","fullyImplemented":true,"id":3,"linearizedBaseContracts":[3],"name":"Errort6","nameLocation":"68:7:0","nodeType":"ContractDefinition","nodes":[],"scope":4,"src":"59:35:0","usedErrors":[]}],"src":"36:84:0"},"id":0}}}
+",
+            "message": "Recovered in ContractDefinition at '}'.",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 120,
+                "file": "A",
+                "start": 119
+            },
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "ast":
+            {
+                "absolutePath": "A",
+                "exportedSymbols":
+                {
+                    "Errort6":
+                    [
+                        3
+                    ]
+                },
+                "id": 4,
+                "license": "GPL-3.0",
+                "nodeType": "SourceUnit",
+                "nodes":
+                [
+                    {
+                        "id": 1,
+                        "literals":
+                        [
+                            "solidity",
+                            ">=",
+                            "0.0"
+                        ],
+                        "nodeType": "PragmaDirective",
+                        "src": "36:22:0"
+                    },
+                    {
+                        "abstract": false,
+                        "baseContracts": [],
+                        "canonicalName": "Errort6",
+                        "contractDependencies": [],
+                        "contractKind": "contract",
+                        "fullyImplemented": true,
+                        "id": 3,
+                        "linearizedBaseContracts":
+                        [
+                            3
+                        ],
+                        "name": "Errort6",
+                        "nameLocation": "68:7:0",
+                        "nodeType": "ContractDefinition",
+                        "nodes": [],
+                        "scope": 4,
+                        "src": "59:35:0",
+                        "usedErrors": []
+                    }
+                ],
+                "src": "36:84:0"
+            },
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_debug_info_in_evm_asm_via_ir_location/output.json

@@ -1,4 +1,13 @@
-{"contracts":{"C":{"C":{"evm":{"assembly":"    /* \"C\":79:428  contract C... */
+{
+    "contracts":
+    {
+        "C":
+        {
+            "C":
+            {
+                "evm":
+                {
+                    "assembly": "    /* \"C\":79:428  contract C... */
   0xa0
   jumpi(tag_5, callvalue)
   0x1f
@@ -361,7 +370,17 @@ sub_0: assembly {
 
     auxdata: <AUXDATA REMOVED>
 }
-"}}},"D":{"D":{"evm":{"assembly":"    /* \"D\":91:166  contract D is C(3)... */
+"
+                }
+            }
+        },
+        "D":
+        {
+            "D":
+            {
+                "evm":
+                {
+                    "assembly": "    /* \"D\":91:166  contract D is C(3)... */
   0xa0
   jumpi(tag_5, callvalue)
   0x1f
@@ -740,4 +759,20 @@ sub_0: assembly {
 
     auxdata: <AUXDATA REMOVED>
 }
-"}}}},"sources":{"C":{"id":0},"D":{"id":1}}}
+"
+                }
+            }
+        }
+    },
+    "sources":
+    {
+        "C":
+        {
+            "id": 0
+        },
+        "D":
+        {
+            "id": 1
+        }
+    }
+}

test/cmdlineTests/standard_debug_info_in_yul_and_evm_asm_print_all/args

@@ -1 +1 @@
---pretty-json --json-indent 4 --allow-paths .
+--allow-paths .

test/cmdlineTests/standard_debug_info_in_yul_and_evm_asm_print_location_only/args

@@ -1 +1 @@
---pretty-json --json-indent 4 --allow-paths .
+--allow-paths .

test/cmdlineTests/standard_debug_info_in_yul_and_evm_asm_print_none/args

@@ -1 +1 @@
---pretty-json --json-indent 4 --allow-paths .
+--allow-paths .

test/cmdlineTests/standard_debug_info_in_yul_and_evm_asm_print_snippet_only/args

@@ -1 +1 @@
---pretty-json --json-indent 4 --allow-paths .
+--allow-paths .

test/cmdlineTests/standard_debug_info_in_yul_location/output.json

@@ -1,4 +1,11 @@
-{"contracts":{"C":{"C":{"ir":"
+{
+    "contracts":
+    {
+        "C":
+        {
+            "C":
+            {
+                "ir": "
 /// @use-src 0:\"C\"
 object \"C_54\" {
     code {
@@ -604,7 +611,8 @@ object \"C_54\" {
 
 }
 
-","irOptimized":"/// @use-src 0:\"C\"
+",
+                "irOptimized": "/// @use-src 0:\"C\"
 object \"C_54\" {
     code {
         {
@@ -759,7 +767,14 @@ object \"C_54\" {
         data \".metadata\" hex\"<BYTECODE REMOVED>\"
     }
 }
-"}},"D":{"D":{"ir":"
+"
+            }
+        },
+        "D":
+        {
+            "D":
+            {
+                "ir": "
 /// @use-src 0:\"C\", 1:\"D\"
 object \"D_72\" {
     code {
@@ -1435,7 +1450,8 @@ object \"D_72\" {
 
 }
 
-","irOptimized":"/// @use-src 0:\"C\", 1:\"D\"
+",
+                "irOptimized": "/// @use-src 0:\"C\", 1:\"D\"
 object \"D_72\" {
     code {
         {
@@ -1597,4 +1613,19 @@ object \"D_72\" {
         data \".metadata\" hex\"<BYTECODE REMOVED>\"
     }
 }
-"}}},"sources":{"C":{"id":0},"D":{"id":1}}}
+"
+            }
+        }
+    },
+    "sources":
+    {
+        "C":
+        {
+            "id": 0
+        },
+        "D":
+        {
+            "id": 1
+        }
+    }
+}

test/cmdlineTests/standard_default_success/output.json

@@ -1 +1,9 @@
-{"sources":{"A":{"id":0}}}
+{
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_empty_file_name/output.json

@@ -1,3 +1,28 @@
-{"errors":[{"component":"general","errorCode":"2904","formattedMessage":"DeclarationError: Declaration \"A\" not found in \"\" (referenced as \".\").
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "2904",
+            "formattedMessage": "DeclarationError: Declaration \"A\" not found in \"\" (referenced as \".\").
 
-","message":"Declaration \"A\" not found in \"\" (referenced as \".\").","severity":"error","sourceLocation":{"end":79,"file":"","start":59},"type":"DeclarationError"}],"sources":{"":{"id":0}}}
+",
+            "message": "Declaration \"A\" not found in \"\" (referenced as \".\").",
+            "severity": "error",
+            "sourceLocation":
+            {
+                "end": 79,
+                "file": "",
+                "start": 59
+            },
+            "type": "DeclarationError"
+        }
+    ],
+    "sources":
+    {
+        "":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_ewasm_requested/output.json

@@ -1,4 +1,14 @@
-{"contracts":{"A":{"C":{"ewasm":{"wasm":"<BYTECODE REMOVED>","wast":"(module
+{
+    "contracts":
+    {
+        "A":
+        {
+            "C":
+            {
+                "ewasm":
+                {
+                    "wasm": "<BYTECODE REMOVED>",
+                    "wast": "(module
     ;; custom section for sub-module
     ;; The Keccak-256 hash of the text representation of <REMOVED>
     ;; (@custom \"C_3_deployed\" \"<BYTECODE REMOVED>\")
@@ -151,4 +161,16 @@
 )
 
 )
-"}}}},"sources":{"A":{"id":0}}}
+"
+                }
+            }
+        }
+    },
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_ewasm_requested_abstract/output.json

@@ -1 +1,23 @@
-{"contracts":{"A":{"C":{"ewasm":{"wasm":"","wast":""}}}},"sources":{"A":{"id":0}}}
+{
+    "contracts":
+    {
+        "A":
+        {
+            "C":
+            {
+                "ewasm":
+                {
+                    "wasm": "",
+                    "wast": ""
+                }
+            }
+        }
+    },
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_function_debug_info/output.json

@@ -1 +1,185 @@
-{"contracts":{"a.sol":{"A":{"evm":{"bytecode":{"functionDebugData":{}},"deployedBytecode":{"functionDebugData":{"@f_19":{"entryPoint":96,"id":19,"parameterSlots":1,"returnSlots":1},"abi_decode_available_length_t_array$_t_uint256_$dyn_memory_ptr":{"entryPoint":439,"id":null,"parameterSlots":3,"returnSlots":1},"abi_decode_t_array$_t_uint256_$dyn_memory_ptr":{"entryPoint":544,"id":null,"parameterSlots":2,"returnSlots":1},"abi_decode_t_uint256":{"entryPoint":418,"id":null,"parameterSlots":2,"returnSlots":1},"abi_decode_tuple_t_array$_t_uint256_$dyn_memory_ptr":{"entryPoint":590,"id":null,"parameterSlots":2,"returnSlots":1},"abi_encode_t_uint256_to_t_uint256_fromStack":{"entryPoint":663,"id":null,"parameterSlots":2,"returnSlots":0},"abi_encode_tuple_t_uint256__to_t_uint256__fromStack_reversed":{"entryPoint":678,"id":null,"parameterSlots":2,"returnSlots":1},"allocate_memory":{"entryPoint":309,"id":null,"parameterSlots":1,"returnSlots":1},"allocate_unbounded":{"entryPoint":171,"id":null,"parameterSlots":0,"returnSlots":1},"array_allocation_size_t_array$_t_uint256_$dyn_memory_ptr":{"entryPoint":336,"id":null,"parameterSlots":1,"returnSlots":1},"checked_add_t_uint256":{"entryPoint":799,"id":null,"parameterSlots":2,"returnSlots":1},"cleanup_t_uint256":{"entryPoint":385,"id":null,"parameterSlots":1,"returnSlots":1},"finalize_allocation":{"entryPoint":260,"id":null,"parameterSlots":2,"returnSlots":0},"panic_error_0x11":{"entryPoint":752,"id":null,"parameterSlots":0,"returnSlots":0},"panic_error_0x32":{"entryPoint":705,"id":null,"parameterSlots":0,"returnSlots":0},"panic_error_0x41":{"entryPoint":213,"id":null,"parameterSlots":0,"returnSlots":0},"revert_error_1b9f4a0a5773e33b91aa01db23bf8c55fce1411167c872835e7fa00a4f17d46d":{"entryPoint":191,"id":null,"parameterSlots":0,"returnSlots":0},"revert_error_81385d8c0b31fffe14be1da910c8bd3a80be4cfa248e04f42ec0faea3132a8ef":{"entryPoint":380,"id":null,"parameterSlots":0,"returnSlots":0},"revert_error_c1322bf8034eace5e0b5c7295db60986aa89aae5e0ea0873e4689e076861a5db":{"entryPoint":186,"id":null,"parameterSlots":0,"returnSlots":0},"revert_error_dbdddcbe895c83990c08b3492a0e83918d802a52331272ac6fdb6a7c4aea3b1b":{"entryPoint":181,"id":null,"parameterSlots":0,"returnSlots":0},"round_up_to_mul_of_32":{"entryPoint":196,"id":null,"parameterSlots":1,"returnSlots":1},"validator_revert_t_uint256":{"entryPoint":395,"id":null,"parameterSlots":1,"returnSlots":0}}}}}}},"sources":{"a.sol":{"id":0}}}
+{
+    "contracts":
+    {
+        "a.sol":
+        {
+            "A":
+            {
+                "evm":
+                {
+                    "bytecode":
+                    {
+                        "functionDebugData": {}
+                    },
+                    "deployedBytecode":
+                    {
+                        "functionDebugData":
+                        {
+                            "@f_19":
+                            {
+                                "entryPoint": 96,
+                                "id": 19,
+                                "parameterSlots": 1,
+                                "returnSlots": 1
+                            },
+                            "abi_decode_available_length_t_array$_t_uint256_$dyn_memory_ptr":
+                            {
+                                "entryPoint": 439,
+                                "id": null,
+                                "parameterSlots": 3,
+                                "returnSlots": 1
+                            },
+                            "abi_decode_t_array$_t_uint256_$dyn_memory_ptr":
+                            {
+                                "entryPoint": 544,
+                                "id": null,
+                                "parameterSlots": 2,
+                                "returnSlots": 1
+                            },
+                            "abi_decode_t_uint256":
+                            {
+                                "entryPoint": 418,
+                                "id": null,
+                                "parameterSlots": 2,
+                                "returnSlots": 1
+                            },
+                            "abi_decode_tuple_t_array$_t_uint256_$dyn_memory_ptr":
+                            {
+                                "entryPoint": 590,
+                                "id": null,
+                                "parameterSlots": 2,
+                                "returnSlots": 1
+                            },
+                            "abi_encode_t_uint256_to_t_uint256_fromStack":
+                            {
+                                "entryPoint": 663,
+                                "id": null,
+                                "parameterSlots": 2,
+                                "returnSlots": 0
+                            },
+                            "abi_encode_tuple_t_uint256__to_t_uint256__fromStack_reversed":
+                            {
+                                "entryPoint": 678,
+                                "id": null,
+                                "parameterSlots": 2,
+                                "returnSlots": 1
+                            },
+                            "allocate_memory":
+                            {
+                                "entryPoint": 309,
+                                "id": null,
+                                "parameterSlots": 1,
+                                "returnSlots": 1
+                            },
+                            "allocate_unbounded":
+                            {
+                                "entryPoint": 171,
+                                "id": null,
+                                "parameterSlots": 0,
+                                "returnSlots": 1
+                            },
+                            "array_allocation_size_t_array$_t_uint256_$dyn_memory_ptr":
+                            {
+                                "entryPoint": 336,
+                                "id": null,
+                                "parameterSlots": 1,
+                                "returnSlots": 1
+                            },
+                            "checked_add_t_uint256":
+                            {
+                                "entryPoint": 799,
+                                "id": null,
+                                "parameterSlots": 2,
+                                "returnSlots": 1
+                            },
+                            "cleanup_t_uint256":
+                            {
+                                "entryPoint": 385,
+                                "id": null,
+                                "parameterSlots": 1,
+                                "returnSlots": 1
+                            },
+                            "finalize_allocation":
+                            {
+                                "entryPoint": 260,
+                                "id": null,
+                                "parameterSlots": 2,
+                                "returnSlots": 0
+                            },
+                            "panic_error_0x11":
+                            {
+                                "entryPoint": 752,
+                                "id": null,
+                                "parameterSlots": 0,
+                                "returnSlots": 0
+                            },
+                            "panic_error_0x32":
+                            {
+                                "entryPoint": 705,
+                                "id": null,
+                                "parameterSlots": 0,
+                                "returnSlots": 0
+                            },
+                            "panic_error_0x41":
+                            {
+                                "entryPoint": 213,
+                                "id": null,
+                                "parameterSlots": 0,
+                                "returnSlots": 0
+                            },
+                            "revert_error_1b9f4a0a5773e33b91aa01db23bf8c55fce1411167c872835e7fa00a4f17d46d":
+                            {
+                                "entryPoint": 191,
+                                "id": null,
+                                "parameterSlots": 0,
+                                "returnSlots": 0
+                            },
+                            "revert_error_81385d8c0b31fffe14be1da910c8bd3a80be4cfa248e04f42ec0faea3132a8ef":
+                            {
+                                "entryPoint": 380,
+                                "id": null,
+                                "parameterSlots": 0,
+                                "returnSlots": 0
+                            },
+                            "revert_error_c1322bf8034eace5e0b5c7295db60986aa89aae5e0ea0873e4689e076861a5db":
+                            {
+                                "entryPoint": 186,
+                                "id": null,
+                                "parameterSlots": 0,
+                                "returnSlots": 0
+                            },
+                            "revert_error_dbdddcbe895c83990c08b3492a0e83918d802a52331272ac6fdb6a7c4aea3b1b":
+                            {
+                                "entryPoint": 181,
+                                "id": null,
+                                "parameterSlots": 0,
+                                "returnSlots": 0
+                            },
+                            "round_up_to_mul_of_32":
+                            {
+                                "entryPoint": 196,
+                                "id": null,
+                                "parameterSlots": 1,
+                                "returnSlots": 1
+                            },
+                            "validator_revert_t_uint256":
+                            {
+                                "entryPoint": 395,
+                                "id": null,
+                                "parameterSlots": 1,
+                                "returnSlots": 0
+                            }
+                        }
+                    }
+                }
+            }
+        }
+    },
+    "sources":
+    {
+        "a.sol":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_immutable_references/output.json

@@ -1 +1,34 @@
-{"contracts":{"a.sol":{"A":{"evm":{"deployedBytecode":{"immutableReferences":{"6":[{"length":32,"start":75}]}}}}}},"sources":{"a.sol":{"id":0}}}
+{
+    "contracts":
+    {
+        "a.sol":
+        {
+            "A":
+            {
+                "evm":
+                {
+                    "deployedBytecode":
+                    {
+                        "immutableReferences":
+                        {
+                            "6":
+                            [
+                                {
+                                    "length": 32,
+                                    "start": 75
+                                }
+                            ]
+                        }
+                    }
+                }
+            }
+        }
+    },
+    "sources":
+    {
+        "a.sol":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_irOptimized_requested/output.json

@@ -1,4 +1,11 @@
-{"contracts":{"A":{"C":{"irOptimized":"/// @use-src 0:\"A\"
+{
+    "contracts":
+    {
+        "A":
+        {
+            "C":
+            {
+                "irOptimized": "/// @use-src 0:\"A\"
 object \"C_7\" {
     code {
         /// @src 0:79:121  \"contract C { function f() public pure {} }\"
@@ -69,4 +76,15 @@ object \"C_7\" {
         data \".metadata\" hex\"<BYTECODE REMOVED>\"
     }
 }
-"}}},"sources":{"A":{"id":0}}}
+"
+            }
+        }
+    },
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_ir_requested/output.json

@@ -1,4 +1,11 @@
-{"contracts":{"A":{"C":{"ir":"
+{
+    "contracts":
+    {
+        "A":
+        {
+            "C":
+            {
+                "ir": "
 /// @use-src 0:\"A\"
 object \"C_7\" {
     code {
@@ -111,4 +118,15 @@ object \"C_7\" {
 
 }
 
-"}}},"sources":{"A":{"id":0}}}
+"
+            }
+        }
+    },
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_method_identifiers_requested/output.json

@@ -1 +1,25 @@
-{"contracts":{"A":{"C":{"evm":{"methodIdentifiers":{"f()":"26121ff0"}}}}},"sources":{"A":{"id":0}}}
+{
+    "contracts":
+    {
+        "A":
+        {
+            "C":
+            {
+                "evm":
+                {
+                    "methodIdentifiers":
+                    {
+                        "f()": "26121ff0"
+                    }
+                }
+            }
+        }
+    },
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_method_identifiers_requested_empty/output.json

@@ -1 +1,22 @@
-{"contracts":{"A":{"C":{"evm":{"methodIdentifiers":{}}}}},"sources":{"A":{"id":0}}}
+{
+    "contracts":
+    {
+        "A":
+        {
+            "C":
+            {
+                "evm":
+                {
+                    "methodIdentifiers": {}
+                }
+            }
+        }
+    },
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_missing_key_useLiteralContent/output.json

@@ -1 +1,9 @@
-{"sources":{"A":{"id":0}}}
+{
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_contracts_all/output.json

@@ -1,4 +1,10 @@
-{"errors":[{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "6328",
+            "formattedMessage": "Warning: CHC: Assertion violation happens here.
 Counterexample:
 
 y = 0
@@ -11,14 +17,28 @@ B.g(0)
 5 | \t\t\t\t\t\tassert(y > 0);
   | \t\t\t\t\t\t^^^^^^^^^^^^^
 
-","message":"CHC: Assertion violation happens here.
+",
+            "message": "CHC: Assertion violation happens here.
 Counterexample:
 
 y = 0
 
 Transaction trace:
 B.constructor()
-B.g(0)","severity":"warning","sourceLocation":{"end":137,"file":"Source","start":124},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
+B.g(0)",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 137,
+                "file": "Source",
+                "start": 124
+            },
+            "type": "Warning"
+        },
+        {
+            "component": "general",
+            "errorCode": "6328",
+            "formattedMessage": "Warning: CHC: Assertion violation happens here.
 Counterexample:
 
 x = 0
@@ -31,11 +51,30 @@ A.f(0)
 10 | \t\t\t\t\t\tassert(x > 0);
    | \t\t\t\t\t\t^^^^^^^^^^^^^
 
-","message":"CHC: Assertion violation happens here.
+",
+            "message": "CHC: Assertion violation happens here.
 Counterexample:
 
 x = 0
 
 Transaction trace:
 A.constructor()
-A.f(0)","severity":"warning","sourceLocation":{"end":231,"file":"Source","start":218},"type":"Warning"}],"sources":{"Source":{"id":0}}}
+A.f(0)",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 231,
+                "file": "Source",
+                "start": 218
+            },
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "Source":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_contracts_all_explicit/output.json

@@ -1,4 +1,10 @@
-{"errors":[{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "6328",
+            "formattedMessage": "Warning: CHC: Assertion violation happens here.
 Counterexample:
 
 y = 0
@@ -11,14 +17,28 @@ B.g(0)
 5 | \t\t\t\t\t\tassert(y > 0);
   | \t\t\t\t\t\t^^^^^^^^^^^^^
 
-","message":"CHC: Assertion violation happens here.
+",
+            "message": "CHC: Assertion violation happens here.
 Counterexample:
 
 y = 0
 
 Transaction trace:
 B.constructor()
-B.g(0)","severity":"warning","sourceLocation":{"end":137,"file":"Source","start":124},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
+B.g(0)",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 137,
+                "file": "Source",
+                "start": 124
+            },
+            "type": "Warning"
+        },
+        {
+            "component": "general",
+            "errorCode": "6328",
+            "formattedMessage": "Warning: CHC: Assertion violation happens here.
 Counterexample:
 
 x = 0
@@ -31,11 +51,30 @@ A.f(0)
 10 | \t\t\t\t\t\tassert(x > 0);
    | \t\t\t\t\t\t^^^^^^^^^^^^^
 
-","message":"CHC: Assertion violation happens here.
+",
+            "message": "CHC: Assertion violation happens here.
 Counterexample:
 
 x = 0
 
 Transaction trace:
 A.constructor()
-A.f(0)","severity":"warning","sourceLocation":{"end":231,"file":"Source","start":218},"type":"Warning"}],"sources":{"Source":{"id":0}}}
+A.f(0)",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 231,
+                "file": "Source",
+                "start": 218
+            },
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "Source":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_contracts_empty_array/output.json

@@ -1 +1,12 @@
-{"errors":[{"component":"general","formattedMessage":"Source contracts must be a non-empty array.","message":"Source contracts must be a non-empty array.","severity":"error","type":"JSONError"}]}
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "formattedMessage": "Source contracts must be a non-empty array.",
+            "message": "Source contracts must be a non-empty array.",
+            "severity": "error",
+            "type": "JSONError"
+        }
+    ]
+}

test/cmdlineTests/standard_model_checker_contracts_empty_contract/output.json

@@ -1 +1,12 @@
-{"errors":[{"component":"general","formattedMessage":"Contract name cannot be empty.","message":"Contract name cannot be empty.","severity":"error","type":"JSONError"}]}
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "formattedMessage": "Contract name cannot be empty.",
+            "message": "Contract name cannot be empty.",
+            "severity": "error",
+            "type": "JSONError"
+        }
+    ]
+}

test/cmdlineTests/standard_model_checker_contracts_empty_source/output.json

@@ -1 +1,12 @@
-{"errors":[{"component":"general","formattedMessage":"Source name cannot be empty.","message":"Source name cannot be empty.","severity":"error","type":"JSONError"}]}
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "formattedMessage": "Source name cannot be empty.",
+            "message": "Source name cannot be empty.",
+            "severity": "error",
+            "type": "JSONError"
+        }
+    ]
+}

test/cmdlineTests/standard_model_checker_contracts_inexistent_contract/output.json

@@ -1,3 +1,22 @@
-{"errors":[{"component":"general","errorCode":"7400","formattedMessage":"Warning: Requested contract \"C\" does not exist in source \"Source\".
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "7400",
+            "formattedMessage": "Warning: Requested contract \"C\" does not exist in source \"Source\".
 
-","message":"Requested contract \"C\" does not exist in source \"Source\".","severity":"warning","type":"Warning"}],"sources":{"Source":{"id":0}}}
+",
+            "message": "Requested contract \"C\" does not exist in source \"Source\".",
+            "severity": "warning",
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "Source":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_contracts_multi_source/output.json

@@ -1,4 +1,10 @@
-{"errors":[{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "6328",
+            "formattedMessage": "Warning: CHC: Assertion violation happens here.
 Counterexample:
 
 y = 0
@@ -11,14 +17,28 @@ B.g(0)
 5 | \t\t\t\t\t\tassert(y > 0);
   | \t\t\t\t\t\t^^^^^^^^^^^^^
 
-","message":"CHC: Assertion violation happens here.
+",
+            "message": "CHC: Assertion violation happens here.
 Counterexample:
 
 y = 0
 
 Transaction trace:
 A.constructor()
-B.g(0)","severity":"warning","sourceLocation":{"end":137,"file":"Source","start":124},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
+B.g(0)",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 137,
+                "file": "Source",
+                "start": 124
+            },
+            "type": "Warning"
+        },
+        {
+            "component": "general",
+            "errorCode": "6328",
+            "formattedMessage": "Warning: CHC: Assertion violation happens here.
 Counterexample:
 
 x = 0
@@ -31,14 +51,28 @@ A.f(0)
 10 | \t\t\t\t\t\tassert(x > 0);
    | \t\t\t\t\t\t^^^^^^^^^^^^^
 
-","message":"CHC: Assertion violation happens here.
+",
+            "message": "CHC: Assertion violation happens here.
 Counterexample:
 
 x = 0
 
 Transaction trace:
 A.constructor()
-A.f(0)","severity":"warning","sourceLocation":{"end":231,"file":"Source","start":218},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
+A.f(0)",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 231,
+                "file": "Source",
+                "start": 218
+            },
+            "type": "Warning"
+        },
+        {
+            "component": "general",
+            "errorCode": "6328",
+            "formattedMessage": "Warning: CHC: Assertion violation happens here.
 Counterexample:
 
 z = 0
@@ -51,11 +85,34 @@ C.h(0)
 6 | \t\t\t\t\t\tassert(z > 100);
   | \t\t\t\t\t\t^^^^^^^^^^^^^^^
 
-","message":"CHC: Assertion violation happens here.
+",
+            "message": "CHC: Assertion violation happens here.
 Counterexample:
 
 z = 0
 
 Transaction trace:
 C.constructor()
-C.h(0)","severity":"warning","sourceLocation":{"end":165,"file":"Source2","start":150},"type":"Warning"}],"sources":{"Source":{"id":0},"Source2":{"id":1}}}
+C.h(0)",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 165,
+                "file": "Source2",
+                "start": 150
+            },
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "Source":
+        {
+            "id": 0
+        },
+        "Source2":
+        {
+            "id": 1
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_contracts_only_one/output.json

@@ -1,4 +1,10 @@
-{"errors":[{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "6328",
+            "formattedMessage": "Warning: CHC: Assertion violation happens here.
 Counterexample:
 
 y = 0
@@ -11,14 +17,28 @@ B.g(0)
 5 | \t\t\t\t\t\tassert(y > 0);
   | \t\t\t\t\t\t^^^^^^^^^^^^^
 
-","message":"CHC: Assertion violation happens here.
+",
+            "message": "CHC: Assertion violation happens here.
 Counterexample:
 
 y = 0
 
 Transaction trace:
 A.constructor()
-B.g(0)","severity":"warning","sourceLocation":{"end":137,"file":"Source","start":124},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
+B.g(0)",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 137,
+                "file": "Source",
+                "start": 124
+            },
+            "type": "Warning"
+        },
+        {
+            "component": "general",
+            "errorCode": "6328",
+            "formattedMessage": "Warning: CHC: Assertion violation happens here.
 Counterexample:
 
 x = 0
@@ -31,11 +51,30 @@ A.f(0)
 10 | \t\t\t\t\t\tassert(x > 0);
    | \t\t\t\t\t\t^^^^^^^^^^^^^
 
-","message":"CHC: Assertion violation happens here.
+",
+            "message": "CHC: Assertion violation happens here.
 Counterexample:
 
 x = 0
 
 Transaction trace:
 A.constructor()
-A.f(0)","severity":"warning","sourceLocation":{"end":231,"file":"Source","start":218},"type":"Warning"}],"sources":{"Source":{"id":0}}}
+A.f(0)",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 231,
+                "file": "Source",
+                "start": 218
+            },
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "Source":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_contracts_wrong_key_sources/output.json

@@ -1,3 +1,22 @@
-{"errors":[{"component":"general","errorCode":"9134","formattedMessage":"Warning: Requested source \"Sourceee\" does not exist.
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "9134",
+            "formattedMessage": "Warning: Requested source \"Sourceee\" does not exist.
 
-","message":"Requested source \"Sourceee\" does not exist.","severity":"warning","type":"Warning"}],"sources":{"Source":{"id":0}}}
+",
+            "message": "Requested source \"Sourceee\" does not exist.",
+            "severity": "warning",
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "Source":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_contracts_wrong_key_sources_2/output.json

@@ -1 +1,12 @@
-{"errors":[{"component":"general","formattedMessage":"settings.modelChecker.contracts is not a JSON object.","message":"settings.modelChecker.contracts is not a JSON object.","severity":"error","type":"JSONError"}]}
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "formattedMessage": "settings.modelChecker.contracts is not a JSON object.",
+            "message": "settings.modelChecker.contracts is not a JSON object.",
+            "severity": "error",
+            "type": "JSONError"
+        }
+    ]
+}

test/cmdlineTests/standard_model_checker_contracts_wrong_key_sources_3/output.json

@@ -1 +1,12 @@
-{"errors":[{"component":"general","formattedMessage":"Source contracts must be an array.","message":"Source contracts must be an array.","severity":"error","type":"JSONError"}]}
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "formattedMessage": "Source contracts must be an array.",
+            "message": "Source contracts must be an array.",
+            "severity": "error",
+            "type": "JSONError"
+        }
+    ]
+}

test/cmdlineTests/standard_model_checker_contracts_wrong_key_sources_4/output.json

@@ -1 +1,12 @@
-{"errors":[{"component":"general","formattedMessage":"Every contract in settings.modelChecker.contracts must be a string.","message":"Every contract in settings.modelChecker.contracts must be a string.","severity":"error","type":"JSONError"}]}
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "formattedMessage": "Every contract in settings.modelChecker.contracts must be a string.",
+            "message": "Every contract in settings.modelChecker.contracts must be a string.",
+            "severity": "error",
+            "type": "JSONError"
+        }
+    ]
+}

test/cmdlineTests/standard_model_checker_divModSlacks_default_all/output.json

@@ -1,4 +1,9 @@
-{"auxiliaryInputRequested":{"smtlib2queries":{"0x72b32f47722af7f889ab5740b229c1799f27d0a693995a581c00f65438255a15":"(set-option :produce-models true)
+{
+    "auxiliaryInputRequested":
+    {
+        "smtlib2queries":
+        {
+            "0x72b32f47722af7f889ab5740b229c1799f27d0a693995a581c00f65438255a15": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |a_3_3| () Int)
 (declare-fun |b_5_3| () Int)
@@ -30,7 +35,8 @@
 
 (assert (and (and (and true true) (and (= expr_15_1 (not (= expr_13_0 expr_14_0))) (and (=> (and true true) true) (and (= expr_14_0 0) (and (=> (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 b_5_0) (and (= _10_0 0) (and (= _8_0 0) (and (and (>= b_5_0 0) (<= b_5_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_3_0 0) (<= a_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 332507694)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 19)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 209)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 170)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 46)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))) (not expr_15_1)))
 (check-sat)
-","0x825b322db572f1c2705128460f2af503aeeb571f1c2e15207ce4fd0355accee6":"(set-option :produce-models true)
+",
+            "0x825b322db572f1c2705128460f2af503aeeb571f1c2e15207ce4fd0355accee6": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |a_3_3| () Int)
 (declare-fun |b_5_3| () Int)
@@ -62,4 +68,14 @@
 
 (assert (and (and (and true true) (and (= expr_15_1 (not (= expr_13_0 expr_14_0))) (and (=> (and true true) true) (and (= expr_14_0 0) (and (=> (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 b_5_0) (and (= _10_0 0) (and (= _8_0 0) (and (and (>= b_5_0 0) (<= b_5_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_3_0 0) (<= a_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 332507694)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 19)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 209)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 170)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 46)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))) expr_15_1))
 (check-sat)
-"}},"sources":{"A":{"id":0}}}
+"
+        }
+    },
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_divModSlacks_default_bmc/output.json

@@ -1,4 +1,9 @@
-{"auxiliaryInputRequested":{"smtlib2queries":{"0x4e97ac0812ea5c46e435c3db54d9e2eb4a3bcadff47f83ce1640429a0a47f6a4":"(set-option :produce-models true)
+{
+    "auxiliaryInputRequested":
+    {
+        "smtlib2queries":
+        {
+            "0x4e97ac0812ea5c46e435c3db54d9e2eb4a3bcadff47f83ce1640429a0a47f6a4": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
 (declare-fun |this_0| () Int)
@@ -47,7 +52,8 @@
 (assert (= |EVALEXPR_4| expr_19_0))
 (check-sat)
 (get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| ))
-","0x5e6c35c70ccbb1d9823ba3ab86fc9448ead56e6158f73aa8bed482232be56105":"(set-option :produce-models true)
+",
+            "0x5e6c35c70ccbb1d9823ba3ab86fc9448ead56e6158f73aa8bed482232be56105": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
 (declare-fun |this_0| () Int)
@@ -96,7 +102,8 @@
 (assert (= |EVALEXPR_4| expr_22_0))
 (check-sat)
 (get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| ))
-","0x615d3f7e7a864c5b3fa9663d698ad3525d0345fa9b53c171d86493beded9023b":"(set-option :produce-models true)
+",
+            "0x615d3f7e7a864c5b3fa9663d698ad3525d0345fa9b53c171d86493beded9023b": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
 (declare-fun |this_0| () Int)
@@ -120,7 +127,8 @@
 
 (assert (and (and (and true true) (and (= expr_15_1 (not (= expr_13_0 expr_14_0))) (and (=> (and true true) true) (and (= expr_14_0 0) (and (=> (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 b_5_0) (and (= _10_0 0) (and (= _8_0 0) (and (and (>= b_5_0 0) (<= b_5_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_3_0 0) (<= a_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 332507694)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 19)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 209)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 170)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 46)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))) (not expr_15_1)))
 (check-sat)
-","0x769f12e07b77225b4e96b3031839452b89976583e45e7924b8bf82ca53a0dd45":"(set-option :produce-models true)
+",
+            "0x769f12e07b77225b4e96b3031839452b89976583e45e7924b8bf82ca53a0dd45": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
 (declare-fun |this_0| () Int)
@@ -144,4 +152,14 @@
 
 (assert (and (and (and true true) (and (= expr_15_1 (not (= expr_13_0 expr_14_0))) (and (=> (and true true) true) (and (= expr_14_0 0) (and (=> (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 b_5_0) (and (= _10_0 0) (and (= _8_0 0) (and (and (>= b_5_0 0) (<= b_5_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_3_0 0) (<= a_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 332507694)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 19)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 209)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 170)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 46)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))) expr_15_1))
 (check-sat)
-"}},"sources":{"A":{"id":0}}}
+"
+        }
+    },
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_divModSlacks_default_chc/output.json

@@ -1 +1,9 @@
-{"sources":{"A":{"id":0}}}
+{
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_divModSlacks_false_all/output.json

@@ -1,4 +1,9 @@
-{"auxiliaryInputRequested":{"smtlib2queries":{"0x591e1d66214247cc99275e22a55210a804c80e9939d5e515cd60a20b3a927c44":"(set-option :produce-models true)
+{
+    "auxiliaryInputRequested":
+    {
+        "smtlib2queries":
+        {
+            "0x591e1d66214247cc99275e22a55210a804c80e9939d5e515cd60a20b3a927c44": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |a_3_3| () Int)
 (declare-fun |b_5_3| () Int)
@@ -51,7 +56,8 @@
 (assert (= |EVALEXPR_4| expr_19_0))
 (check-sat)
 (get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| ))
-","0x5d07befb0482a6d4e328641d57f10a2cbc89b2c287f8d5630bbe20ba4f829e7d":"(set-option :produce-models true)
+",
+            "0x5d07befb0482a6d4e328641d57f10a2cbc89b2c287f8d5630bbe20ba4f829e7d": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |a_3_3| () Int)
 (declare-fun |b_5_3| () Int)
@@ -104,7 +110,8 @@
 (assert (= |EVALEXPR_4| expr_22_0))
 (check-sat)
 (get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| ))
-","0x72b32f47722af7f889ab5740b229c1799f27d0a693995a581c00f65438255a15":"(set-option :produce-models true)
+",
+            "0x72b32f47722af7f889ab5740b229c1799f27d0a693995a581c00f65438255a15": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |a_3_3| () Int)
 (declare-fun |b_5_3| () Int)
@@ -136,7 +143,8 @@
 
 (assert (and (and (and true true) (and (= expr_15_1 (not (= expr_13_0 expr_14_0))) (and (=> (and true true) true) (and (= expr_14_0 0) (and (=> (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 b_5_0) (and (= _10_0 0) (and (= _8_0 0) (and (and (>= b_5_0 0) (<= b_5_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_3_0 0) (<= a_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 332507694)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 19)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 209)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 170)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 46)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))) (not expr_15_1)))
 (check-sat)
-","0x825b322db572f1c2705128460f2af503aeeb571f1c2e15207ce4fd0355accee6":"(set-option :produce-models true)
+",
+            "0x825b322db572f1c2705128460f2af503aeeb571f1c2e15207ce4fd0355accee6": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |a_3_3| () Int)
 (declare-fun |b_5_3| () Int)
@@ -168,18 +176,67 @@
 
 (assert (and (and (and true true) (and (= expr_15_1 (not (= expr_13_0 expr_14_0))) (and (=> (and true true) true) (and (= expr_14_0 0) (and (=> (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 b_5_0) (and (= _10_0 0) (and (= _8_0 0) (and (and (>= b_5_0 0) (<= b_5_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_3_0 0) (<= a_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 332507694)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 19)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 209)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 170)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 46)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))) expr_15_1))
 (check-sat)
-"}},"errors":[{"component":"general","errorCode":"1218","formattedMessage":"Warning: CHC: Error trying to invoke SMT solver.
+"
+        }
+    },
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "1218",
+            "formattedMessage": "Warning: CHC: Error trying to invoke SMT solver.
  --> A:7:15:
   |
 7 | \t\t\t\t\t\treturn (a / b, a % b);
   | \t\t\t\t\t\t        ^^^^^
 
-","message":"CHC: Error trying to invoke SMT solver.","severity":"warning","sourceLocation":{"end":182,"file":"A","start":177},"type":"Warning"},{"component":"general","errorCode":"1218","formattedMessage":"Warning: CHC: Error trying to invoke SMT solver.
+",
+            "message": "CHC: Error trying to invoke SMT solver.",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 182,
+                "file": "A",
+                "start": 177
+            },
+            "type": "Warning"
+        },
+        {
+            "component": "general",
+            "errorCode": "1218",
+            "formattedMessage": "Warning: CHC: Error trying to invoke SMT solver.
  --> A:7:22:
   |
 7 | \t\t\t\t\t\treturn (a / b, a % b);
   | \t\t\t\t\t\t               ^^^^^
 
-","message":"CHC: Error trying to invoke SMT solver.","severity":"warning","sourceLocation":{"end":189,"file":"A","start":184},"type":"Warning"},{"component":"general","errorCode":"5840","formattedMessage":"Warning: CHC: 2 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
+",
+            "message": "CHC: Error trying to invoke SMT solver.",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 189,
+                "file": "A",
+                "start": 184
+            },
+            "type": "Warning"
+        },
+        {
+            "component": "general",
+            "errorCode": "5840",
+            "formattedMessage": "Warning: CHC: 2 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
 
-","message":"CHC: 2 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.","severity":"warning","type":"Warning"}],"sources":{"A":{"id":0}}}
+",
+            "message": "CHC: 2 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.",
+            "severity": "warning",
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_divModSlacks_false_bmc/output.json

@@ -1,4 +1,9 @@
-{"auxiliaryInputRequested":{"smtlib2queries":{"0x615d3f7e7a864c5b3fa9663d698ad3525d0345fa9b53c171d86493beded9023b":"(set-option :produce-models true)
+{
+    "auxiliaryInputRequested":
+    {
+        "smtlib2queries":
+        {
+            "0x615d3f7e7a864c5b3fa9663d698ad3525d0345fa9b53c171d86493beded9023b": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
 (declare-fun |this_0| () Int)
@@ -22,7 +27,8 @@
 
 (assert (and (and (and true true) (and (= expr_15_1 (not (= expr_13_0 expr_14_0))) (and (=> (and true true) true) (and (= expr_14_0 0) (and (=> (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 b_5_0) (and (= _10_0 0) (and (= _8_0 0) (and (and (>= b_5_0 0) (<= b_5_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_3_0 0) (<= a_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 332507694)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 19)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 209)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 170)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 46)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))) (not expr_15_1)))
 (check-sat)
-","0x769f12e07b77225b4e96b3031839452b89976583e45e7924b8bf82ca53a0dd45":"(set-option :produce-models true)
+",
+            "0x769f12e07b77225b4e96b3031839452b89976583e45e7924b8bf82ca53a0dd45": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
 (declare-fun |this_0| () Int)
@@ -46,7 +52,8 @@
 
 (assert (and (and (and true true) (and (= expr_15_1 (not (= expr_13_0 expr_14_0))) (and (=> (and true true) true) (and (= expr_14_0 0) (and (=> (and true true) (and (>= expr_13_0 0) (<= expr_13_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_0 b_5_0) (and (= _10_0 0) (and (= _8_0 0) (and (and (>= b_5_0 0) (<= b_5_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_3_0 0) (<= a_3_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 332507694)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 19)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 209)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 170)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 46)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))))))))) expr_15_1))
 (check-sat)
-","0x7eae514917329522604efe7292b9036d26ff191c3e65dfa51c727b3e7427c10b":"(set-option :produce-models true)
+",
+            "0x7eae514917329522604efe7292b9036d26ff191c3e65dfa51c727b3e7427c10b": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
 (declare-fun |this_0| () Int)
@@ -91,7 +98,8 @@
 (assert (= |EVALEXPR_4| expr_19_0))
 (check-sat)
 (get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| ))
-","0xda96cf77e7e434e73e6c4dd847b2e0aa96dbdebf7a585f884ff024246977d02a":"(set-option :produce-models true)
+",
+            "0xda96cf77e7e434e73e6c4dd847b2e0aa96dbdebf7a585f884ff024246977d02a": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
 (declare-fun |this_0| () Int)
@@ -136,4 +144,14 @@
 (assert (= |EVALEXPR_4| expr_22_0))
 (check-sat)
 (get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| |EVALEXPR_3| |EVALEXPR_4| ))
-"}},"sources":{"A":{"id":0}}}
+"
+        }
+    },
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_divModSlacks_false_chc/output.json

@@ -1,15 +1,62 @@
-{"errors":[{"component":"general","errorCode":"1218","formattedMessage":"Warning: CHC: Error trying to invoke SMT solver.
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "1218",
+            "formattedMessage": "Warning: CHC: Error trying to invoke SMT solver.
  --> A:7:15:
   |
 7 | \t\t\t\t\t\treturn (a / b, a % b);
   | \t\t\t\t\t\t        ^^^^^
 
-","message":"CHC: Error trying to invoke SMT solver.","severity":"warning","sourceLocation":{"end":182,"file":"A","start":177},"type":"Warning"},{"component":"general","errorCode":"1218","formattedMessage":"Warning: CHC: Error trying to invoke SMT solver.
+",
+            "message": "CHC: Error trying to invoke SMT solver.",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 182,
+                "file": "A",
+                "start": 177
+            },
+            "type": "Warning"
+        },
+        {
+            "component": "general",
+            "errorCode": "1218",
+            "formattedMessage": "Warning: CHC: Error trying to invoke SMT solver.
  --> A:7:22:
   |
 7 | \t\t\t\t\t\treturn (a / b, a % b);
   | \t\t\t\t\t\t               ^^^^^
 
-","message":"CHC: Error trying to invoke SMT solver.","severity":"warning","sourceLocation":{"end":189,"file":"A","start":184},"type":"Warning"},{"component":"general","errorCode":"5840","formattedMessage":"Warning: CHC: 2 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
+",
+            "message": "CHC: Error trying to invoke SMT solver.",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 189,
+                "file": "A",
+                "start": 184
+            },
+            "type": "Warning"
+        },
+        {
+            "component": "general",
+            "errorCode": "5840",
+            "formattedMessage": "Warning: CHC: 2 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
 
-","message":"CHC: 2 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.","severity":"warning","type":"Warning"}],"sources":{"A":{"id":0}}}
+",
+            "message": "CHC: 2 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.",
+            "severity": "warning",
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_divModSlacks_wrong/output.json

@@ -1 +1,12 @@
-{"errors":[{"component":"general","formattedMessage":"settings.modelChecker.divModNoSlacks must be a Boolean.","message":"settings.modelChecker.divModNoSlacks must be a Boolean.","severity":"error","type":"JSONError"}]}
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "formattedMessage": "settings.modelChecker.divModNoSlacks must be a Boolean.",
+            "message": "settings.modelChecker.divModNoSlacks must be a Boolean.",
+            "severity": "error",
+            "type": "JSONError"
+        }
+    ]
+}

test/cmdlineTests/standard_model_checker_engine_all/output.json

@@ -1,4 +1,10 @@
-{"errors":[{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "6328",
+            "formattedMessage": "Warning: CHC: Assertion violation happens here.
 Counterexample:
 
 x = 0
@@ -11,11 +17,30 @@ C.f(0)
 4 | contract C { function f(uint x) public pure { assert(x > 0); } }
   |                                               ^^^^^^^^^^^^^
 
-","message":"CHC: Assertion violation happens here.
+",
+            "message": "CHC: Assertion violation happens here.
 Counterexample:
 
 x = 0
 
 Transaction trace:
 C.constructor()
-C.f(0)","severity":"warning","sourceLocation":{"end":119,"file":"A","start":106},"type":"Warning"}],"sources":{"A":{"id":0}}}
+C.f(0)",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 119,
+                "file": "A",
+                "start": 106
+            },
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_engine_bmc/output.json

@@ -1,4 +1,9 @@
-{"auxiliaryInputRequested":{"smtlib2queries":{"0x7fe5be7672be6bc9bc2b750f3170bfa08ecd79fc95afb084539b74294c2dd24d":"(set-option :produce-models true)
+{
+    "auxiliaryInputRequested":
+    {
+        "smtlib2queries":
+        {
+            "0x7fe5be7672be6bc9bc2b750f3170bfa08ecd79fc95afb084539b74294c2dd24d": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
 (declare-fun |this_0| () Int)
@@ -22,7 +27,15 @@
 (assert (= |EVALEXPR_0| x_3_0))
 (check-sat)
 (get-value (|EVALEXPR_0| ))
-"}},"errors":[{"component":"general","errorCode":"4661","formattedMessage":"Warning: BMC: Assertion violation happens here.
+"
+        }
+    },
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "4661",
+            "formattedMessage": "Warning: BMC: Assertion violation happens here.
  --> A:4:47:
   |
 4 | contract C { function f(uint x) public pure { assert(x > 0); } }
@@ -33,6 +46,37 @@ Note: Counterexample:
 Note: Callstack:
 Note:
 
-","message":"BMC: Assertion violation happens here.","secondarySourceLocations":[{"message":"Counterexample:
+",
+            "message": "BMC: Assertion violation happens here.",
+            "secondarySourceLocations":
+            [
+                {
+                    "message": "Counterexample:
   x = 0
-"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":119,"file":"A","start":106},"type":"Warning"}],"sources":{"A":{"id":0}}}
+"
+                },
+                {
+                    "message": "Callstack:"
+                },
+                {
+                    "message": ""
+                }
+            ],
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 119,
+                "file": "A",
+                "start": 106
+            },
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_engine_chc/output.json

@@ -1,4 +1,10 @@
-{"errors":[{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "6328",
+            "formattedMessage": "Warning: CHC: Assertion violation happens here.
 Counterexample:
 
 x = 0
@@ -11,11 +17,30 @@ C.f(0)
 4 | contract C { function f(uint x) public pure { assert(x > 0); } }
   |                                               ^^^^^^^^^^^^^
 
-","message":"CHC: Assertion violation happens here.
+",
+            "message": "CHC: Assertion violation happens here.
 Counterexample:
 
 x = 0
 
 Transaction trace:
 C.constructor()
-C.f(0)","severity":"warning","sourceLocation":{"end":119,"file":"A","start":106},"type":"Warning"}],"sources":{"A":{"id":0}}}
+C.f(0)",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 119,
+                "file": "A",
+                "start": 106
+            },
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_engine_none/output.json

@@ -1 +1,9 @@
-{"sources":{"A":{"id":0}}}
+{
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_invariants_contract/output.json

@@ -1,7 +1,26 @@
-{"errors":[{"component":"general","errorCode":"1180","formattedMessage":"Info: Contract invariant(s) for A:test:
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "1180",
+            "formattedMessage": "Info: Contract invariant(s) for A:test:
 ((x <= 0) || true)
 
 
-","message":"Contract invariant(s) for A:test:
+",
+            "message": "Contract invariant(s) for A:test:
 ((x <= 0) || true)
-","severity":"info","type":"Info"}],"sources":{"A":{"id":0}}}
+",
+            "severity": "info",
+            "type": "Info"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_invariants_contract_reentrancy/output.json

@@ -1,10 +1,30 @@
-{"errors":[{"component":"general","errorCode":"9302","formattedMessage":"Warning: Return value of low-level calls not used.
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "9302",
+            "formattedMessage": "Warning: Return value of low-level calls not used.
  --> A:7:7:
   |
 7 | \t\t\t\t\t\t_a.call(\"\");
   | \t\t\t\t\t\t^^^^^^^^^^^
 
-","message":"Return value of low-level calls not used.","severity":"warning","sourceLocation":{"end":143,"file":"A","start":132},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
+",
+            "message": "Return value of low-level calls not used.",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 143,
+                "file": "A",
+                "start": 132
+            },
+            "type": "Warning"
+        },
+        {
+            "component": "general",
+            "errorCode": "6328",
+            "formattedMessage": "Warning: CHC: Assertion violation happens here.
 Counterexample:
 x = 0
 _a = 0x0
@@ -19,7 +39,8 @@ test.f(0x0)
 8 | \t\t\t\t\t\tassert(x == 10);
   | \t\t\t\t\t\t^^^^^^^^^^^^^^^
 
-","message":"CHC: Assertion violation happens here.
+",
+            "message": "CHC: Assertion violation happens here.
 Counterexample:
 x = 0
 _a = 0x0
@@ -28,4 +49,22 @@ Transaction trace:
 test.constructor()
 State: x = 0
 test.f(0x0)
-    _a.call(\"\") -- untrusted external call","severity":"warning","sourceLocation":{"end":166,"file":"A","start":151},"type":"Warning"}],"sources":{"A":{"id":0}}}
+    _a.call(\"\") -- untrusted external call",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 166,
+                "file": "A",
+                "start": 151
+            },
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_invariants_reentrancy/output.json

@@ -1,17 +1,50 @@
-{"errors":[{"component":"general","errorCode":"9302","formattedMessage":"Warning: Return value of low-level calls not used.
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "9302",
+            "formattedMessage": "Warning: Return value of low-level calls not used.
  --> A:7:7:
   |
 7 | \t\t\t\t\t\t_a.call(\"\");
   | \t\t\t\t\t\t^^^^^^^^^^^
 
-","message":"Return value of low-level calls not used.","severity":"warning","sourceLocation":{"end":143,"file":"A","start":132},"type":"Warning"},{"component":"general","errorCode":"1180","formattedMessage":"Info: Reentrancy property(ies) for A:test:
+",
+            "message": "Return value of low-level calls not used.",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 143,
+                "file": "A",
+                "start": 132
+            },
+            "type": "Warning"
+        },
+        {
+            "component": "general",
+            "errorCode": "1180",
+            "formattedMessage": "Info: Reentrancy property(ies) for A:test:
 (((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0))) || true)
 <errorCode> = 0 -> no errors
 <errorCode> = 1 -> Assertion failed at assert(x < 10)
 
 
-","message":"Reentrancy property(ies) for A:test:
+",
+            "message": "Reentrancy property(ies) for A:test:
 (((!(x <= 0) || (x' <= 0)) && (!(x <= 0) || (<errorCode> <= 0))) || true)
 <errorCode> = 0 -> no errors
 <errorCode> = 1 -> Assertion failed at assert(x < 10)
-","severity":"info","type":"Info"}],"sources":{"A":{"id":0}}}
+",
+            "severity": "info",
+            "type": "Info"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_invariants_wrong_key/output.json

@@ -1 +1,12 @@
-{"errors":[{"component":"general","formattedMessage":"Invalid model checker invariants requested.","message":"Invalid model checker invariants requested.","severity":"error","type":"JSONError"}]}
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "formattedMessage": "Invalid model checker invariants requested.",
+            "message": "Invalid model checker invariants requested.",
+            "severity": "error",
+            "type": "JSONError"
+        }
+    ]
+}

test/cmdlineTests/standard_model_checker_invariants_wrong_type/output.json

@@ -1 +1,12 @@
-{"errors":[{"component":"general","formattedMessage":"Every invariant type in settings.modelChecker.invariants must be a string.","message":"Every invariant type in settings.modelChecker.invariants must be a string.","severity":"error","type":"JSONError"}]}
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "formattedMessage": "Every invariant type in settings.modelChecker.invariants must be a string.",
+            "message": "Every invariant type in settings.modelChecker.invariants must be a string.",
+            "severity": "error",
+            "type": "JSONError"
+        }
+    ]
+}

test/cmdlineTests/standard_model_checker_invariants_wrong_type_2/output.json

@@ -1 +1,12 @@
-{"errors":[{"component":"general","formattedMessage":"settings.modelChecker.invariants must be an array.","message":"settings.modelChecker.invariants must be an array.","severity":"error","type":"JSONError"}]}
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "formattedMessage": "settings.modelChecker.invariants must be an array.",
+            "message": "settings.modelChecker.invariants must be an array.",
+            "severity": "error",
+            "type": "JSONError"
+        }
+    ]
+}

test/cmdlineTests/standard_model_checker_show_unproved_default_all_engines/output.json

@@ -1,4 +1,9 @@
-{"auxiliaryInputRequested":{"smtlib2queries":{"0x4cd81a462deca8d6bf08b33a7f5bce9cf9306c7ee90b83c106ca7927066a23b1":"(set-option :produce-models true)
+{
+    "auxiliaryInputRequested":
+    {
+        "smtlib2queries":
+        {
+            "0x4cd81a462deca8d6bf08b33a7f5bce9cf9306c7ee90b83c106ca7927066a23b1": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-datatypes ((|struct test.S| 0)) (((|struct test.S| (|struct test.S_accessor_x| Int)))))
 (declare-fun |s_7_3| () |struct test.S|)
@@ -24,7 +29,8 @@
 
 (assert (and (and (and true true) (and (= expr_15_0 b_9_0) (and true (and true (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 2562959041)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 152)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 195)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 166)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))) (not expr_15_0)))
 (check-sat)
-","0x65d23088fadc165b70d1947e1ba5191db247c8c5fab4e23d292c1168e94b4784":"(set-option :produce-models true)
+",
+            "0x65d23088fadc165b70d1947e1ba5191db247c8c5fab4e23d292c1168e94b4784": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-datatypes ((|struct test.S| 0)) (((|struct test.S| (|struct test.S_accessor_x| Int)))))
 (declare-fun |s_7_3| () |struct test.S|)
@@ -69,7 +75,8 @@
 (assert (= |EVALEXPR_0| b_9_0))
 (check-sat)
 (get-value (|EVALEXPR_0| ))
-","0xd6dbbd7b7e45b0360943223d07028611980d896347710102f264ffa0ae086fad":"(set-option :produce-models true)
+",
+            "0xd6dbbd7b7e45b0360943223d07028611980d896347710102f264ffa0ae086fad": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-datatypes ((|struct test.S| 0)) (((|struct test.S| (|struct test.S_accessor_x| Int)))))
 (declare-fun |s_7_3| () |struct test.S|)
@@ -95,8 +102,37 @@
 
 (assert (and (and (and true true) (and (= expr_15_0 b_9_0) (and true (and true (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 2562959041)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 152)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 195)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 166)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))) expr_15_0))
 (check-sat)
-"}},"errors":[{"component":"general","errorCode":"5840","formattedMessage":"Warning: CHC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
+"
+        }
+    },
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "5840",
+            "formattedMessage": "Warning: CHC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
 
-","message":"CHC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.","severity":"warning","type":"Warning"},{"component":"general","errorCode":"2788","formattedMessage":"Warning: BMC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
+",
+            "message": "CHC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.",
+            "severity": "warning",
+            "type": "Warning"
+        },
+        {
+            "component": "general",
+            "errorCode": "2788",
+            "formattedMessage": "Warning: BMC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
 
-","message":"BMC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.","severity":"warning","type":"Warning"}],"sources":{"A":{"id":0}}}
+",
+            "message": "BMC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.",
+            "severity": "warning",
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_show_unproved_false_all_engines/output.json

@@ -1,4 +1,9 @@
-{"auxiliaryInputRequested":{"smtlib2queries":{"0x4cd81a462deca8d6bf08b33a7f5bce9cf9306c7ee90b83c106ca7927066a23b1":"(set-option :produce-models true)
+{
+    "auxiliaryInputRequested":
+    {
+        "smtlib2queries":
+        {
+            "0x4cd81a462deca8d6bf08b33a7f5bce9cf9306c7ee90b83c106ca7927066a23b1": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-datatypes ((|struct test.S| 0)) (((|struct test.S| (|struct test.S_accessor_x| Int)))))
 (declare-fun |s_7_3| () |struct test.S|)
@@ -24,7 +29,8 @@
 
 (assert (and (and (and true true) (and (= expr_15_0 b_9_0) (and true (and true (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 2562959041)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 152)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 195)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 166)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))) (not expr_15_0)))
 (check-sat)
-","0x65d23088fadc165b70d1947e1ba5191db247c8c5fab4e23d292c1168e94b4784":"(set-option :produce-models true)
+",
+            "0x65d23088fadc165b70d1947e1ba5191db247c8c5fab4e23d292c1168e94b4784": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-datatypes ((|struct test.S| 0)) (((|struct test.S| (|struct test.S_accessor_x| Int)))))
 (declare-fun |s_7_3| () |struct test.S|)
@@ -69,7 +75,8 @@
 (assert (= |EVALEXPR_0| b_9_0))
 (check-sat)
 (get-value (|EVALEXPR_0| ))
-","0xd6dbbd7b7e45b0360943223d07028611980d896347710102f264ffa0ae086fad":"(set-option :produce-models true)
+",
+            "0xd6dbbd7b7e45b0360943223d07028611980d896347710102f264ffa0ae086fad": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-datatypes ((|struct test.S| 0)) (((|struct test.S| (|struct test.S_accessor_x| Int)))))
 (declare-fun |s_7_3| () |struct test.S|)
@@ -95,8 +102,37 @@
 
 (assert (and (and (and true true) (and (= expr_15_0 b_9_0) (and true (and true (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 2562959041)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 152)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 195)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 166)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))) expr_15_0))
 (check-sat)
-"}},"errors":[{"component":"general","errorCode":"5840","formattedMessage":"Warning: CHC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
+"
+        }
+    },
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "5840",
+            "formattedMessage": "Warning: CHC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
 
-","message":"CHC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.","severity":"warning","type":"Warning"},{"component":"general","errorCode":"2788","formattedMessage":"Warning: BMC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
+",
+            "message": "CHC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.",
+            "severity": "warning",
+            "type": "Warning"
+        },
+        {
+            "component": "general",
+            "errorCode": "2788",
+            "formattedMessage": "Warning: BMC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
 
-","message":"BMC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.","severity":"warning","type":"Warning"}],"sources":{"A":{"id":0}}}
+",
+            "message": "BMC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.",
+            "severity": "warning",
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_show_unproved_false_bmc/output.json

@@ -1,4 +1,9 @@
-{"auxiliaryInputRequested":{"smtlib2queries":{"0x5953b22204605efc775a59974aec3ddf9f831e46e30a65e149873e6f48887590":"(set-option :produce-models true)
+{
+    "auxiliaryInputRequested":
+    {
+        "smtlib2queries":
+        {
+            "0x5953b22204605efc775a59974aec3ddf9f831e46e30a65e149873e6f48887590": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
 (declare-fun |this_0| () Int)
@@ -20,7 +25,8 @@
 
 (assert (and (and (and true true) (and (= expr_15_0 b_9_0) (and true (and true (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 2562959041)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 152)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 195)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 166)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))) (not expr_15_0)))
 (check-sat)
-","0x84635fcc37e5318fb46619945199a333750ee247769e97445a2f89b98b54fef9":"(set-option :produce-models true)
+",
+            "0x84635fcc37e5318fb46619945199a333750ee247769e97445a2f89b98b54fef9": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
 (declare-fun |this_0| () Int)
@@ -61,7 +67,8 @@
 (assert (= |EVALEXPR_0| b_9_0))
 (check-sat)
 (get-value (|EVALEXPR_0| ))
-","0xd55ef003dcd6e8ebbd55fce4adaa36b4d898204d649e5426179dea4b7450a9f5":"(set-option :produce-models true)
+",
+            "0xd55ef003dcd6e8ebbd55fce4adaa36b4d898204d649e5426179dea4b7450a9f5": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
 (declare-fun |this_0| () Int)
@@ -83,6 +90,27 @@
 
 (assert (and (and (and true true) (and (= expr_15_0 b_9_0) (and true (and true (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 2562959041)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 152)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 195)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 166)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))) expr_15_0))
 (check-sat)
-"}},"errors":[{"component":"general","errorCode":"2788","formattedMessage":"Warning: BMC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
+"
+        }
+    },
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "2788",
+            "formattedMessage": "Warning: BMC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
 
-","message":"BMC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.","severity":"warning","type":"Warning"}],"sources":{"A":{"id":0}}}
+",
+            "message": "BMC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.",
+            "severity": "warning",
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_show_unproved_false_chc/output.json

@@ -1,3 +1,22 @@
-{"errors":[{"component":"general","errorCode":"5840","formattedMessage":"Warning: CHC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "5840",
+            "formattedMessage": "Warning: CHC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
 
-","message":"CHC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.","severity":"warning","type":"Warning"}],"sources":{"A":{"id":0}}}
+",
+            "message": "CHC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.",
+            "severity": "warning",
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_show_unproved_true_all_engines/output.json

@@ -1,4 +1,9 @@
-{"auxiliaryInputRequested":{"smtlib2queries":{"0x4cd81a462deca8d6bf08b33a7f5bce9cf9306c7ee90b83c106ca7927066a23b1":"(set-option :produce-models true)
+{
+    "auxiliaryInputRequested":
+    {
+        "smtlib2queries":
+        {
+            "0x4cd81a462deca8d6bf08b33a7f5bce9cf9306c7ee90b83c106ca7927066a23b1": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-datatypes ((|struct test.S| 0)) (((|struct test.S| (|struct test.S_accessor_x| Int)))))
 (declare-fun |s_7_3| () |struct test.S|)
@@ -24,7 +29,8 @@
 
 (assert (and (and (and true true) (and (= expr_15_0 b_9_0) (and true (and true (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 2562959041)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 152)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 195)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 166)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))) (not expr_15_0)))
 (check-sat)
-","0x65d23088fadc165b70d1947e1ba5191db247c8c5fab4e23d292c1168e94b4784":"(set-option :produce-models true)
+",
+            "0x65d23088fadc165b70d1947e1ba5191db247c8c5fab4e23d292c1168e94b4784": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-datatypes ((|struct test.S| 0)) (((|struct test.S| (|struct test.S_accessor_x| Int)))))
 (declare-fun |s_7_3| () |struct test.S|)
@@ -69,7 +75,8 @@
 (assert (= |EVALEXPR_0| b_9_0))
 (check-sat)
 (get-value (|EVALEXPR_0| ))
-","0xd6dbbd7b7e45b0360943223d07028611980d896347710102f264ffa0ae086fad":"(set-option :produce-models true)
+",
+            "0xd6dbbd7b7e45b0360943223d07028611980d896347710102f264ffa0ae086fad": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-datatypes ((|struct test.S| 0)) (((|struct test.S| (|struct test.S_accessor_x| Int)))))
 (declare-fun |s_7_3| () |struct test.S|)
@@ -95,17 +102,64 @@
 
 (assert (and (and (and true true) (and (= expr_15_0 b_9_0) (and true (and true (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 2562959041)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 152)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 195)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 166)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))) expr_15_0))
 (check-sat)
-"}},"errors":[{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation might happen here.
+"
+        }
+    },
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "6328",
+            "formattedMessage": "Warning: CHC: Assertion violation might happen here.
   --> A:11:7:
    |
 11 | \t\t\t\t\t\tassert(s.x > 0);
    | \t\t\t\t\t\t^^^^^^^^^^^^^^^
 
-","message":"CHC: Assertion violation might happen here.","severity":"warning","sourceLocation":{"end":201,"file":"A","start":186},"type":"Warning"},{"component":"general","errorCode":"7812","formattedMessage":"Warning: BMC: Assertion violation might happen here.
+",
+            "message": "CHC: Assertion violation might happen here.",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 201,
+                "file": "A",
+                "start": 186
+            },
+            "type": "Warning"
+        },
+        {
+            "component": "general",
+            "errorCode": "7812",
+            "formattedMessage": "Warning: BMC: Assertion violation might happen here.
   --> A:11:7:
    |
 11 | \t\t\t\t\t\tassert(s.x > 0);
    | \t\t\t\t\t\t^^^^^^^^^^^^^^^
 Note:
 
-","message":"BMC: Assertion violation might happen here.","secondarySourceLocations":[{"message":""}],"severity":"warning","sourceLocation":{"end":201,"file":"A","start":186},"type":"Warning"}],"sources":{"A":{"id":0}}}
+",
+            "message": "BMC: Assertion violation might happen here.",
+            "secondarySourceLocations":
+            [
+                {
+                    "message": ""
+                }
+            ],
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 201,
+                "file": "A",
+                "start": 186
+            },
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_show_unproved_true_bmc/output.json

@@ -1,4 +1,9 @@
-{"auxiliaryInputRequested":{"smtlib2queries":{"0x5953b22204605efc775a59974aec3ddf9f831e46e30a65e149873e6f48887590":"(set-option :produce-models true)
+{
+    "auxiliaryInputRequested":
+    {
+        "smtlib2queries":
+        {
+            "0x5953b22204605efc775a59974aec3ddf9f831e46e30a65e149873e6f48887590": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
 (declare-fun |this_0| () Int)
@@ -20,7 +25,8 @@
 
 (assert (and (and (and true true) (and (= expr_15_0 b_9_0) (and true (and true (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 2562959041)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 152)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 195)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 166)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))) (not expr_15_0)))
 (check-sat)
-","0x84635fcc37e5318fb46619945199a333750ee247769e97445a2f89b98b54fef9":"(set-option :produce-models true)
+",
+            "0x84635fcc37e5318fb46619945199a333750ee247769e97445a2f89b98b54fef9": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
 (declare-fun |this_0| () Int)
@@ -61,7 +67,8 @@
 (assert (= |EVALEXPR_0| b_9_0))
 (check-sat)
 (get-value (|EVALEXPR_0| ))
-","0xd55ef003dcd6e8ebbd55fce4adaa36b4d898204d649e5426179dea4b7450a9f5":"(set-option :produce-models true)
+",
+            "0xd55ef003dcd6e8ebbd55fce4adaa36b4d898204d649e5426179dea4b7450a9f5": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
 (declare-fun |this_0| () Int)
@@ -83,11 +90,44 @@
 
 (assert (and (and (and true true) (and (= expr_15_0 b_9_0) (and true (and true (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 2562959041)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 152)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 195)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 166)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true))))) expr_15_0))
 (check-sat)
-"}},"errors":[{"component":"general","errorCode":"7812","formattedMessage":"Warning: BMC: Assertion violation might happen here.
+"
+        }
+    },
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "7812",
+            "formattedMessage": "Warning: BMC: Assertion violation might happen here.
   --> A:11:7:
    |
 11 | \t\t\t\t\t\tassert(s.x > 0);
    | \t\t\t\t\t\t^^^^^^^^^^^^^^^
 Note:
 
-","message":"BMC: Assertion violation might happen here.","secondarySourceLocations":[{"message":""}],"severity":"warning","sourceLocation":{"end":201,"file":"A","start":186},"type":"Warning"}],"sources":{"A":{"id":0}}}
+",
+            "message": "BMC: Assertion violation might happen here.",
+            "secondarySourceLocations":
+            [
+                {
+                    "message": ""
+                }
+            ],
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 201,
+                "file": "A",
+                "start": 186
+            },
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_show_unproved_true_chc/output.json

@@ -1,7 +1,32 @@
-{"errors":[{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation might happen here.
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "6328",
+            "formattedMessage": "Warning: CHC: Assertion violation might happen here.
   --> A:11:7:
    |
 11 | \t\t\t\t\t\tassert(s.x > 0);
    | \t\t\t\t\t\t^^^^^^^^^^^^^^^
 
-","message":"CHC: Assertion violation might happen here.","severity":"warning","sourceLocation":{"end":201,"file":"A","start":186},"type":"Warning"}],"sources":{"A":{"id":0}}}
+",
+            "message": "CHC: Assertion violation might happen here.",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 201,
+                "file": "A",
+                "start": 186
+            },
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_show_unproved_wrong/output.json

@@ -1 +1,12 @@
-{"errors":[{"component":"general","formattedMessage":"settings.modelChecker.showUnproved must be a Boolean value.","message":"settings.modelChecker.showUnproved must be a Boolean value.","severity":"error","type":"JSONError"}]}
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "formattedMessage": "settings.modelChecker.showUnproved must be a Boolean value.",
+            "message": "settings.modelChecker.showUnproved must be a Boolean value.",
+            "severity": "error",
+            "type": "JSONError"
+        }
+    ]
+}

test/cmdlineTests/standard_model_checker_solvers_all/output.json

@@ -1,4 +1,10 @@
-{"errors":[{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "6328",
+            "formattedMessage": "Warning: CHC: Assertion violation happens here.
 Counterexample:
 
 x = 0
@@ -11,11 +17,30 @@ C.f(0)
 4 | contract C { function f(uint x) public pure { assert(x > 0); } }
   |                                               ^^^^^^^^^^^^^
 
-","message":"CHC: Assertion violation happens here.
+",
+            "message": "CHC: Assertion violation happens here.
 Counterexample:
 
 x = 0
 
 Transaction trace:
 C.constructor()
-C.f(0)","severity":"warning","sourceLocation":{"end":119,"file":"A","start":106},"type":"Warning"}],"sources":{"A":{"id":0}}}
+C.f(0)",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 119,
+                "file": "A",
+                "start": 106
+            },
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_solvers_none/output.json

@@ -1,5 +1,32 @@
-{"errors":[{"component":"general","errorCode":"7649","formattedMessage":"Warning: CHC analysis was not possible since no Horn solver was found and enabled.
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "7649",
+            "formattedMessage": "Warning: CHC analysis was not possible since no Horn solver was found and enabled.
 
-","message":"CHC analysis was not possible since no Horn solver was found and enabled.","severity":"warning","type":"Warning"},{"component":"general","errorCode":"7710","formattedMessage":"Warning: BMC analysis was not possible since no SMT solver was found and enabled.
+",
+            "message": "CHC analysis was not possible since no Horn solver was found and enabled.",
+            "severity": "warning",
+            "type": "Warning"
+        },
+        {
+            "component": "general",
+            "errorCode": "7710",
+            "formattedMessage": "Warning: BMC analysis was not possible since no SMT solver was found and enabled.
 
-","message":"BMC analysis was not possible since no SMT solver was found and enabled.","severity":"warning","type":"Warning"}],"sources":{"A":{"id":0}}}
+",
+            "message": "BMC analysis was not possible since no SMT solver was found and enabled.",
+            "severity": "warning",
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_solvers_smtlib2/output.json

@@ -1,4 +1,9 @@
-{"auxiliaryInputRequested":{"smtlib2queries":{"0x2bcd3328dc8d31e869efd5e0dfdb16a6fa26f0a9c2829ea55670262be485e401":"(set-option :produce-models true)
+{
+    "auxiliaryInputRequested":
+    {
+        "smtlib2queries":
+        {
+            "0x2bcd3328dc8d31e869efd5e0dfdb16a6fa26f0a9c2829ea55670262be485e401": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |x_3_3| () Int)
 (declare-fun |error_0| () Int)
@@ -24,7 +29,8 @@
 (assert (= |EVALEXPR_0| x_3_0))
 (check-sat)
 (get-value (|EVALEXPR_0| ))
-","0x4e70784a8a93c7429a716aa8b778f3de5d1f63b30158452534da5d44e5967d2b":"(set-logic HORN)
+",
+            "0x4e70784a8a93c7429a716aa8b778f3de5d1f63b30158452534da5d44e5967d2b": "(set-logic HORN)
 
 (declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))
 (declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int)))))
@@ -145,12 +151,57 @@
 (assert
 (forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (x_3_0 Int) (x_3_1 Int) (x_3_2 Int))
 (=> error_target_3_0 false)))
-(check-sat)"}},"errors":[{"component":"general","errorCode":"5840","formattedMessage":"Warning: CHC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
+(check-sat)"
+        }
+    },
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "5840",
+            "formattedMessage": "Warning: CHC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
 
-","message":"CHC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.","severity":"warning","type":"Warning"},{"component":"general","errorCode":"3996","formattedMessage":"Warning: CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled.
+",
+            "message": "CHC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.",
+            "severity": "warning",
+            "type": "Warning"
+        },
+        {
+            "component": "general",
+            "errorCode": "3996",
+            "formattedMessage": "Warning: CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled.
 
-","message":"CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled.","severity":"warning","type":"Warning"},{"component":"general","errorCode":"2788","formattedMessage":"Warning: BMC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
+",
+            "message": "CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled.",
+            "severity": "warning",
+            "type": "Warning"
+        },
+        {
+            "component": "general",
+            "errorCode": "2788",
+            "formattedMessage": "Warning: BMC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.
 
-","message":"BMC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.","severity":"warning","type":"Warning"},{"component":"general","errorCode":"8084","formattedMessage":"Warning: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled.
+",
+            "message": "BMC: 1 verification condition(s) could not be proved. Enable the model checker option \"show unproved\" to see all of them. Consider choosing a specific contract to be verified in order to reduce the solving problems. Consider increasing the timeout per query.",
+            "severity": "warning",
+            "type": "Warning"
+        },
+        {
+            "component": "general",
+            "errorCode": "8084",
+            "formattedMessage": "Warning: BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled.
 
-","message":"BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled.","severity":"warning","type":"Warning"}],"sources":{"A":{"id":0}}}
+",
+            "message": "BMC analysis was not possible. No SMT solver (Z3 or CVC4) was available. None of the installed solvers was enabled.",
+            "severity": "warning",
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_solvers_z3/output.json

@@ -1,4 +1,10 @@
-{"errors":[{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "6328",
+            "formattedMessage": "Warning: CHC: Assertion violation happens here.
 Counterexample:
 
 x = 0
@@ -11,11 +17,30 @@ C.f(0)
 4 | contract C { function f(uint x) public pure { assert(x > 0); } }
   |                                               ^^^^^^^^^^^^^
 
-","message":"CHC: Assertion violation happens here.
+",
+            "message": "CHC: Assertion violation happens here.
 Counterexample:
 
 x = 0
 
 Transaction trace:
 C.constructor()
-C.f(0)","severity":"warning","sourceLocation":{"end":119,"file":"A","start":106},"type":"Warning"}],"sources":{"A":{"id":0}}}
+C.f(0)",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 119,
+                "file": "A",
+                "start": 106
+            },
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_solvers_z3_smtlib2/output.json

@@ -1,4 +1,10 @@
-{"errors":[{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "6328",
+            "formattedMessage": "Warning: CHC: Assertion violation happens here.
 Counterexample:
 
 x = 0
@@ -11,11 +17,30 @@ C.f(0)
 4 | contract C { function f(uint x) public pure { assert(x > 0); } }
   |                                               ^^^^^^^^^^^^^
 
-","message":"CHC: Assertion violation happens here.
+",
+            "message": "CHC: Assertion violation happens here.
 Counterexample:
 
 x = 0
 
 Transaction trace:
 C.constructor()
-C.f(0)","severity":"warning","sourceLocation":{"end":119,"file":"A","start":106},"type":"Warning"}],"sources":{"A":{"id":0}}}
+C.f(0)",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 119,
+                "file": "A",
+                "start": 106
+            },
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_targets_assert_bmc/output.json

@@ -1,4 +1,9 @@
-{"auxiliaryInputRequested":{"smtlib2queries":{"0x67f6235b42fbb5cc636b1d18ccd5622020b45eef0c634965f9adf8b4bb923a64":"(set-option :produce-models true)
+{
+    "auxiliaryInputRequested":
+    {
+        "smtlib2queries":
+        {
+            "0x67f6235b42fbb5cc636b1d18ccd5622020b45eef0c634965f9adf8b4bb923a64": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
 (declare-fun |this_0| () Int)
@@ -53,7 +58,15 @@
 (assert (= |EVALEXPR_1| x_8_1))
 (check-sat)
 (get-value (|EVALEXPR_0| |EVALEXPR_1| ))
-"}},"errors":[{"component":"general","errorCode":"4661","formattedMessage":"Warning: BMC: Assertion violation happens here.
+"
+        }
+    },
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "4661",
+            "formattedMessage": "Warning: BMC: Assertion violation happens here.
   --> A:12:7:
    |
 12 | \t\t\t\t\t\tassert(x > 0);
@@ -65,7 +78,38 @@ Note: Counterexample:
 Note: Callstack:
 Note:
 
-","message":"BMC: Assertion violation happens here.","secondarySourceLocations":[{"message":"Counterexample:
+",
+            "message": "BMC: Assertion violation happens here.",
+            "secondarySourceLocations":
+            [
+                {
+                    "message": "Counterexample:
   a = 0
   x = 0
-"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":258,"file":"A","start":245},"type":"Warning"}],"sources":{"A":{"id":0}}}
+"
+                },
+                {
+                    "message": "Callstack:"
+                },
+                {
+                    "message": ""
+                }
+            ],
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 258,
+                "file": "A",
+                "start": 245
+            },
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_targets_assert_chc/output.json

@@ -1,4 +1,10 @@
-{"errors":[{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "6328",
+            "formattedMessage": "Warning: CHC: Assertion violation happens here.
 Counterexample:
 arr = []
 a = 0x0
@@ -13,7 +19,8 @@ test.f(0x0, 1)
 12 | \t\t\t\t\t\tassert(x > 0);
    | \t\t\t\t\t\t^^^^^^^^^^^^^
 
-","message":"CHC: Assertion violation happens here.
+",
+            "message": "CHC: Assertion violation happens here.
 Counterexample:
 arr = []
 a = 0x0
@@ -22,4 +29,22 @@ x = 0
 Transaction trace:
 test.constructor()
 State: arr = []
-test.f(0x0, 1)","severity":"warning","sourceLocation":{"end":258,"file":"A","start":245},"type":"Warning"}],"sources":{"A":{"id":0}}}
+test.f(0x0, 1)",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 258,
+                "file": "A",
+                "start": 245
+            },
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_targets_balance_bmc/output.json

@@ -1,4 +1,9 @@
-{"auxiliaryInputRequested":{"smtlib2queries":{"0xa5a6f54f166338793f025832fad8408fccb5fa0ee7a8ab0cb4ed7ec5a8c034de":"(set-option :produce-models true)
+{
+    "auxiliaryInputRequested":
+    {
+        "smtlib2queries":
+        {
+            "0xa5a6f54f166338793f025832fad8408fccb5fa0ee7a8ab0cb4ed7ec5a8c034de": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
 (declare-fun |this_0| () Int)
@@ -53,7 +58,15 @@
 (assert (= |EVALEXPR_1| x_8_1))
 (check-sat)
 (get-value (|EVALEXPR_0| |EVALEXPR_1| ))
-"}},"errors":[{"component":"general","errorCode":"1236","formattedMessage":"Warning: BMC: Insufficient funds happens here.
+"
+        }
+    },
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "1236",
+            "formattedMessage": "Warning: BMC: Insufficient funds happens here.
   --> A:11:7:
    |
 11 | \t\t\t\t\t\ta.transfer(x);
@@ -65,7 +78,38 @@ Note: Counterexample:
 Note: Callstack:
 Note:
 
-","message":"BMC: Insufficient funds happens here.","secondarySourceLocations":[{"message":"Counterexample:
+",
+            "message": "BMC: Insufficient funds happens here.",
+            "secondarySourceLocations":
+            [
+                {
+                    "message": "Counterexample:
   a = 0
   x = 0
-"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":237,"file":"A","start":224},"type":"Warning"}],"sources":{"A":{"id":0}}}
+"
+                },
+                {
+                    "message": "Callstack:"
+                },
+                {
+                    "message": ""
+                }
+            ],
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 237,
+                "file": "A",
+                "start": 224
+            },
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_targets_balance_chc/output.json

@@ -1 +1,9 @@
-{"sources":{"A":{"id":0}}}
+{
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_targets_constantCondition_bmc/output.json

@@ -1,4 +1,9 @@
-{"auxiliaryInputRequested":{"smtlib2queries":{"0xca9972ec543d923e2e93a20db0b793a19de392a072a70371f575dbee55fe301c":"(set-option :produce-models true)
+{
+    "auxiliaryInputRequested":
+    {
+        "smtlib2queries":
+        {
+            "0xca9972ec543d923e2e93a20db0b793a19de392a072a70371f575dbee55fe301c": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
 (declare-fun |this_0| () Int)
@@ -23,7 +28,8 @@
 
 (assert (and (and (and true true) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (=> (and true true) true) (and (= expr_13_0 0) (and (=> (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint_array_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))) (not expr_14_1)))
 (check-sat)
-","0xdda5d43b30361d8d706472ecb9bb78f49c5beb6ffe9eba3ff632d1cd5f17e317":"(set-option :produce-models true)
+",
+            "0xdda5d43b30361d8d706472ecb9bb78f49c5beb6ffe9eba3ff632d1cd5f17e317": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
 (declare-fun |this_0| () Int)
@@ -48,11 +54,44 @@
 
 (assert (and (and (and true true) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (=> (and true true) true) (and (= expr_13_0 0) (and (=> (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint_array_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))) expr_14_1))
 (check-sat)
-"}},"errors":[{"component":"general","errorCode":"6838","formattedMessage":"Warning: BMC: Condition is always true.
+"
+        }
+    },
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "6838",
+            "formattedMessage": "Warning: BMC: Condition is always true.
  --> A:7:15:
   |
 7 | \t\t\t\t\t\trequire(x >= 0);
   | \t\t\t\t\t\t        ^^^^^^
 Note: Callstack:
 
-","message":"BMC: Condition is always true.","secondarySourceLocations":[{"message":"Callstack:"}],"severity":"warning","sourceLocation":{"end":165,"file":"A","start":159},"type":"Warning"}],"sources":{"A":{"id":0}}}
+",
+            "message": "BMC: Condition is always true.",
+            "secondarySourceLocations":
+            [
+                {
+                    "message": "Callstack:"
+                }
+            ],
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 165,
+                "file": "A",
+                "start": 159
+            },
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_targets_constantCondition_chc/output.json

@@ -1 +1,9 @@
-{"sources":{"A":{"id":0}}}
+{
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_targets_default_all_engines/output.json

@@ -1,4 +1,9 @@
-{"auxiliaryInputRequested":{"smtlib2queries":{"0x03d0edb825a4f6251a71019a2075e51c5d4fce6236dfaa9b24ed56309b4cb52e":"(set-option :produce-models true)
+{
+    "auxiliaryInputRequested":
+    {
+        "smtlib2queries":
+        {
+            "0x03d0edb825a4f6251a71019a2075e51c5d4fce6236dfaa9b24ed56309b4cb52e": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-datatypes ((|uint_array_tuple| 0)) (((|uint_array_tuple| (|uint_array_tuple_accessor_array| (Array Int Int)) (|uint_array_tuple_accessor_length| Int)))))
 (declare-fun |arr_4_length_pair_2| () |uint_array_tuple|)
@@ -30,7 +35,8 @@
 
 (assert (and (and (and true true) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (=> (and true true) true) (and (= expr_13_0 0) (and (=> (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint_array_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))) (not expr_14_1)))
 (check-sat)
-","0xa7b2de16abc4c0f0f9e2c540a576178d99cb73a01cf0d0d1d62d51735c6d3b44":"(set-option :produce-models true)
+",
+            "0xa7b2de16abc4c0f0f9e2c540a576178d99cb73a01cf0d0d1d62d51735c6d3b44": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-datatypes ((|uint_array_tuple| 0)) (((|uint_array_tuple| (|uint_array_tuple_accessor_array| (Array Int Int)) (|uint_array_tuple_accessor_length| Int)))))
 (declare-fun |arr_4_length_pair_2| () |uint_array_tuple|)
@@ -91,7 +97,8 @@
 (assert (= |EVALEXPR_1| x_8_1))
 (check-sat)
 (get-value (|EVALEXPR_0| |EVALEXPR_1| ))
-","0xd43cc6edbb2db7e490ff38b099043a3d3f17f85031b33673e76cb1eaf0598122":"(set-option :produce-models true)
+",
+            "0xd43cc6edbb2db7e490ff38b099043a3d3f17f85031b33673e76cb1eaf0598122": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-datatypes ((|uint_array_tuple| 0)) (((|uint_array_tuple| (|uint_array_tuple_accessor_array| (Array Int Int)) (|uint_array_tuple_accessor_length| Int)))))
 (declare-fun |arr_4_length_pair_2| () |uint_array_tuple|)
@@ -123,7 +130,15 @@
 
 (assert (and (and (and true true) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (=> (and true true) true) (and (= expr_13_0 0) (and (=> (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint_array_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))) expr_14_1))
 (check-sat)
-"}},"errors":[{"component":"general","errorCode":"4281","formattedMessage":"Warning: CHC: Division by zero happens here.
+"
+        }
+    },
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "4281",
+            "formattedMessage": "Warning: CHC: Division by zero happens here.
 Counterexample:
 arr = []
 a = 0x0
@@ -138,7 +153,8 @@ test.f(0x0, 1)
 10 | \t\t\t\t\t\t2 / x;
    | \t\t\t\t\t\t^^^^^
 
-","message":"CHC: Division by zero happens here.
+",
+            "message": "CHC: Division by zero happens here.
 Counterexample:
 arr = []
 a = 0x0
@@ -147,7 +163,20 @@ x = 0
 Transaction trace:
 test.constructor()
 State: arr = []
-test.f(0x0, 1)","severity":"warning","sourceLocation":{"end":216,"file":"A","start":211},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
+test.f(0x0, 1)",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 216,
+                "file": "A",
+                "start": 211
+            },
+            "type": "Warning"
+        },
+        {
+            "component": "general",
+            "errorCode": "6328",
+            "formattedMessage": "Warning: CHC: Assertion violation happens here.
 Counterexample:
 arr = []
 a = 0x0
@@ -162,7 +191,8 @@ test.f(0x0, 1)
 12 | \t\t\t\t\t\tassert(x > 0);
    | \t\t\t\t\t\t^^^^^^^^^^^^^
 
-","message":"CHC: Assertion violation happens here.
+",
+            "message": "CHC: Assertion violation happens here.
 Counterexample:
 arr = []
 a = 0x0
@@ -171,7 +201,20 @@ x = 0
 Transaction trace:
 test.constructor()
 State: arr = []
-test.f(0x0, 1)","severity":"warning","sourceLocation":{"end":258,"file":"A","start":245},"type":"Warning"},{"component":"general","errorCode":"2529","formattedMessage":"Warning: CHC: Empty array \"pop\" happens here.
+test.f(0x0, 1)",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 258,
+                "file": "A",
+                "start": 245
+            },
+            "type": "Warning"
+        },
+        {
+            "component": "general",
+            "errorCode": "2529",
+            "formattedMessage": "Warning: CHC: Empty array \"pop\" happens here.
 Counterexample:
 arr = []
 a = 0x0
@@ -186,7 +229,8 @@ test.f(0x0, 1)
 13 | \t\t\t\t\t\tarr.pop();
    | \t\t\t\t\t\t^^^^^^^^^
 
-","message":"CHC: Empty array \"pop\" happens here.
+",
+            "message": "CHC: Empty array \"pop\" happens here.
 Counterexample:
 arr = []
 a = 0x0
@@ -195,7 +239,20 @@ x = 0
 Transaction trace:
 test.constructor()
 State: arr = []
-test.f(0x0, 1)","severity":"warning","sourceLocation":{"end":275,"file":"A","start":266},"type":"Warning"},{"component":"general","errorCode":"6368","formattedMessage":"Warning: CHC: Out of bounds access happens here.
+test.f(0x0, 1)",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 275,
+                "file": "A",
+                "start": 266
+            },
+            "type": "Warning"
+        },
+        {
+            "component": "general",
+            "errorCode": "6368",
+            "formattedMessage": "Warning: CHC: Out of bounds access happens here.
 Counterexample:
 arr = []
 a = 0x0
@@ -210,7 +267,8 @@ test.f(0x0, 1)
 14 | \t\t\t\t\t\tarr[x];
    | \t\t\t\t\t\t^^^^^^
 
-","message":"CHC: Out of bounds access happens here.
+",
+            "message": "CHC: Out of bounds access happens here.
 Counterexample:
 arr = []
 a = 0x0
@@ -219,14 +277,47 @@ x = 0
 Transaction trace:
 test.constructor()
 State: arr = []
-test.f(0x0, 1)","severity":"warning","sourceLocation":{"end":289,"file":"A","start":283},"type":"Warning"},{"component":"general","errorCode":"6838","formattedMessage":"Warning: BMC: Condition is always true.
+test.f(0x0, 1)",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 289,
+                "file": "A",
+                "start": 283
+            },
+            "type": "Warning"
+        },
+        {
+            "component": "general",
+            "errorCode": "6838",
+            "formattedMessage": "Warning: BMC: Condition is always true.
  --> A:7:15:
   |
 7 | \t\t\t\t\t\trequire(x >= 0);
   | \t\t\t\t\t\t        ^^^^^^
 Note: Callstack:
 
-","message":"BMC: Condition is always true.","secondarySourceLocations":[{"message":"Callstack:"}],"severity":"warning","sourceLocation":{"end":165,"file":"A","start":159},"type":"Warning"},{"component":"general","errorCode":"1236","formattedMessage":"Warning: BMC: Insufficient funds happens here.
+",
+            "message": "BMC: Condition is always true.",
+            "secondarySourceLocations":
+            [
+                {
+                    "message": "Callstack:"
+                }
+            ],
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 165,
+                "file": "A",
+                "start": 159
+            },
+            "type": "Warning"
+        },
+        {
+            "component": "general",
+            "errorCode": "1236",
+            "formattedMessage": "Warning: BMC: Insufficient funds happens here.
   --> A:11:7:
    |
 11 | \t\t\t\t\t\ta.transfer(x);
@@ -238,7 +329,38 @@ Note: Counterexample:
 Note: Callstack:
 Note:
 
-","message":"BMC: Insufficient funds happens here.","secondarySourceLocations":[{"message":"Counterexample:
+",
+            "message": "BMC: Insufficient funds happens here.",
+            "secondarySourceLocations":
+            [
+                {
+                    "message": "Counterexample:
   a = 0
   x = 0
-"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":237,"file":"A","start":224},"type":"Warning"}],"sources":{"A":{"id":0}}}
+"
+                },
+                {
+                    "message": "Callstack:"
+                },
+                {
+                    "message": ""
+                }
+            ],
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 237,
+                "file": "A",
+                "start": 224
+            },
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_targets_default_bmc/output.json

@@ -1,4 +1,9 @@
-{"auxiliaryInputRequested":{"smtlib2queries":{"0x540d6a4b18ea4181713b8f0e9b4b272f762e142ba1716a3960cfdbed3f1ae64e":"(set-option :produce-models true)
+{
+    "auxiliaryInputRequested":
+    {
+        "smtlib2queries":
+        {
+            "0x540d6a4b18ea4181713b8f0e9b4b272f762e142ba1716a3960cfdbed3f1ae64e": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
 (declare-fun |this_0| () Int)
@@ -55,7 +60,8 @@
 (assert (= |EVALEXPR_2| expr_29_0))
 (check-sat)
 (get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| ))
-","0x67f6235b42fbb5cc636b1d18ccd5622020b45eef0c634965f9adf8b4bb923a64":"(set-option :produce-models true)
+",
+            "0x67f6235b42fbb5cc636b1d18ccd5622020b45eef0c634965f9adf8b4bb923a64": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
 (declare-fun |this_0| () Int)
@@ -110,7 +116,8 @@
 (assert (= |EVALEXPR_1| x_8_1))
 (check-sat)
 (get-value (|EVALEXPR_0| |EVALEXPR_1| ))
-","0xa5a6f54f166338793f025832fad8408fccb5fa0ee7a8ab0cb4ed7ec5a8c034de":"(set-option :produce-models true)
+",
+            "0xa5a6f54f166338793f025832fad8408fccb5fa0ee7a8ab0cb4ed7ec5a8c034de": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
 (declare-fun |this_0| () Int)
@@ -165,7 +172,8 @@
 (assert (= |EVALEXPR_1| x_8_1))
 (check-sat)
 (get-value (|EVALEXPR_0| |EVALEXPR_1| ))
-","0xca9972ec543d923e2e93a20db0b793a19de392a072a70371f575dbee55fe301c":"(set-option :produce-models true)
+",
+            "0xca9972ec543d923e2e93a20db0b793a19de392a072a70371f575dbee55fe301c": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
 (declare-fun |this_0| () Int)
@@ -190,7 +198,8 @@
 
 (assert (and (and (and true true) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (=> (and true true) true) (and (= expr_13_0 0) (and (=> (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint_array_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))) (not expr_14_1)))
 (check-sat)
-","0xdda5d43b30361d8d706472ecb9bb78f49c5beb6ffe9eba3ff632d1cd5f17e317":"(set-option :produce-models true)
+",
+            "0xdda5d43b30361d8d706472ecb9bb78f49c5beb6ffe9eba3ff632d1cd5f17e317": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
 (declare-fun |this_0| () Int)
@@ -215,14 +224,42 @@
 
 (assert (and (and (and true true) (and (= expr_14_1 (>= expr_12_0 expr_13_0)) (and (=> (and true true) true) (and (= expr_13_0 0) (and (=> (and true true) (and (>= expr_12_0 0) (<= expr_12_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_12_0 x_8_0) (and (and (>= x_8_0 0) (<= x_8_0 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (and (>= a_6_0 0) (<= a_6_0 1461501637330902918203684832716283019655932542975)) (and (>= (|uint_array_tuple_accessor_length| arr_4_length_pair_1) 0) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 1917212865)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 114)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 70)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 88)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 193)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) true)))))))))) expr_14_1))
 (check-sat)
-"}},"errors":[{"component":"general","errorCode":"6838","formattedMessage":"Warning: BMC: Condition is always true.
+"
+        }
+    },
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "6838",
+            "formattedMessage": "Warning: BMC: Condition is always true.
  --> A:7:15:
   |
 7 | \t\t\t\t\t\trequire(x >= 0);
   | \t\t\t\t\t\t        ^^^^^^
 Note: Callstack:
 
-","message":"BMC: Condition is always true.","secondarySourceLocations":[{"message":"Callstack:"}],"severity":"warning","sourceLocation":{"end":165,"file":"A","start":159},"type":"Warning"},{"component":"general","errorCode":"3046","formattedMessage":"Warning: BMC: Division by zero happens here.
+",
+            "message": "BMC: Condition is always true.",
+            "secondarySourceLocations":
+            [
+                {
+                    "message": "Callstack:"
+                }
+            ],
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 165,
+                "file": "A",
+                "start": 159
+            },
+            "type": "Warning"
+        },
+        {
+            "component": "general",
+            "errorCode": "3046",
+            "formattedMessage": "Warning: BMC: Division by zero happens here.
   --> A:10:7:
    |
 10 | \t\t\t\t\t\t2 / x;
@@ -235,11 +272,37 @@ Note: Counterexample:
 Note: Callstack:
 Note:
 
-","message":"BMC: Division by zero happens here.","secondarySourceLocations":[{"message":"Counterexample:
+",
+            "message": "BMC: Division by zero happens here.",
+            "secondarySourceLocations":
+            [
+                {
+                    "message": "Counterexample:
   <result> = 0
   a = 0
   x = 0
-"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":216,"file":"A","start":211},"type":"Warning"},{"component":"general","errorCode":"1236","formattedMessage":"Warning: BMC: Insufficient funds happens here.
+"
+                },
+                {
+                    "message": "Callstack:"
+                },
+                {
+                    "message": ""
+                }
+            ],
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 216,
+                "file": "A",
+                "start": 211
+            },
+            "type": "Warning"
+        },
+        {
+            "component": "general",
+            "errorCode": "1236",
+            "formattedMessage": "Warning: BMC: Insufficient funds happens here.
   --> A:11:7:
    |
 11 | \t\t\t\t\t\ta.transfer(x);
@@ -251,10 +314,36 @@ Note: Counterexample:
 Note: Callstack:
 Note:
 
-","message":"BMC: Insufficient funds happens here.","secondarySourceLocations":[{"message":"Counterexample:
+",
+            "message": "BMC: Insufficient funds happens here.",
+            "secondarySourceLocations":
+            [
+                {
+                    "message": "Counterexample:
   a = 0
   x = 0
-"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":237,"file":"A","start":224},"type":"Warning"},{"component":"general","errorCode":"4661","formattedMessage":"Warning: BMC: Assertion violation happens here.
+"
+                },
+                {
+                    "message": "Callstack:"
+                },
+                {
+                    "message": ""
+                }
+            ],
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 237,
+                "file": "A",
+                "start": 224
+            },
+            "type": "Warning"
+        },
+        {
+            "component": "general",
+            "errorCode": "4661",
+            "formattedMessage": "Warning: BMC: Assertion violation happens here.
   --> A:12:7:
    |
 12 | \t\t\t\t\t\tassert(x > 0);
@@ -266,7 +355,38 @@ Note: Counterexample:
 Note: Callstack:
 Note:
 
-","message":"BMC: Assertion violation happens here.","secondarySourceLocations":[{"message":"Counterexample:
+",
+            "message": "BMC: Assertion violation happens here.",
+            "secondarySourceLocations":
+            [
+                {
+                    "message": "Counterexample:
   a = 0
   x = 0
-"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":258,"file":"A","start":245},"type":"Warning"}],"sources":{"A":{"id":0}}}
+"
+                },
+                {
+                    "message": "Callstack:"
+                },
+                {
+                    "message": ""
+                }
+            ],
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 258,
+                "file": "A",
+                "start": 245
+            },
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_targets_default_chc/output.json

@@ -1,4 +1,10 @@
-{"errors":[{"component":"general","errorCode":"4281","formattedMessage":"Warning: CHC: Division by zero happens here.
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "4281",
+            "formattedMessage": "Warning: CHC: Division by zero happens here.
 Counterexample:
 arr = []
 a = 0x0
@@ -13,7 +19,8 @@ test.f(0x0, 1)
 10 | \t\t\t\t\t\t2 / x;
    | \t\t\t\t\t\t^^^^^
 
-","message":"CHC: Division by zero happens here.
+",
+            "message": "CHC: Division by zero happens here.
 Counterexample:
 arr = []
 a = 0x0
@@ -22,7 +29,20 @@ x = 0
 Transaction trace:
 test.constructor()
 State: arr = []
-test.f(0x0, 1)","severity":"warning","sourceLocation":{"end":216,"file":"A","start":211},"type":"Warning"},{"component":"general","errorCode":"6328","formattedMessage":"Warning: CHC: Assertion violation happens here.
+test.f(0x0, 1)",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 216,
+                "file": "A",
+                "start": 211
+            },
+            "type": "Warning"
+        },
+        {
+            "component": "general",
+            "errorCode": "6328",
+            "formattedMessage": "Warning: CHC: Assertion violation happens here.
 Counterexample:
 arr = []
 a = 0x0
@@ -37,7 +57,8 @@ test.f(0x0, 1)
 12 | \t\t\t\t\t\tassert(x > 0);
    | \t\t\t\t\t\t^^^^^^^^^^^^^
 
-","message":"CHC: Assertion violation happens here.
+",
+            "message": "CHC: Assertion violation happens here.
 Counterexample:
 arr = []
 a = 0x0
@@ -46,7 +67,20 @@ x = 0
 Transaction trace:
 test.constructor()
 State: arr = []
-test.f(0x0, 1)","severity":"warning","sourceLocation":{"end":258,"file":"A","start":245},"type":"Warning"},{"component":"general","errorCode":"2529","formattedMessage":"Warning: CHC: Empty array \"pop\" happens here.
+test.f(0x0, 1)",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 258,
+                "file": "A",
+                "start": 245
+            },
+            "type": "Warning"
+        },
+        {
+            "component": "general",
+            "errorCode": "2529",
+            "formattedMessage": "Warning: CHC: Empty array \"pop\" happens here.
 Counterexample:
 arr = []
 a = 0x0
@@ -61,7 +95,8 @@ test.f(0x0, 1)
 13 | \t\t\t\t\t\tarr.pop();
    | \t\t\t\t\t\t^^^^^^^^^
 
-","message":"CHC: Empty array \"pop\" happens here.
+",
+            "message": "CHC: Empty array \"pop\" happens here.
 Counterexample:
 arr = []
 a = 0x0
@@ -70,7 +105,20 @@ x = 0
 Transaction trace:
 test.constructor()
 State: arr = []
-test.f(0x0, 1)","severity":"warning","sourceLocation":{"end":275,"file":"A","start":266},"type":"Warning"},{"component":"general","errorCode":"6368","formattedMessage":"Warning: CHC: Out of bounds access happens here.
+test.f(0x0, 1)",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 275,
+                "file": "A",
+                "start": 266
+            },
+            "type": "Warning"
+        },
+        {
+            "component": "general",
+            "errorCode": "6368",
+            "formattedMessage": "Warning: CHC: Out of bounds access happens here.
 Counterexample:
 arr = []
 a = 0x0
@@ -85,7 +133,8 @@ test.f(0x0, 1)
 14 | \t\t\t\t\t\tarr[x];
    | \t\t\t\t\t\t^^^^^^
 
-","message":"CHC: Out of bounds access happens here.
+",
+            "message": "CHC: Out of bounds access happens here.
 Counterexample:
 arr = []
 a = 0x0
@@ -94,4 +143,22 @@ x = 0
 Transaction trace:
 test.constructor()
 State: arr = []
-test.f(0x0, 1)","severity":"warning","sourceLocation":{"end":289,"file":"A","start":283},"type":"Warning"}],"sources":{"A":{"id":0}}}
+test.f(0x0, 1)",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 289,
+                "file": "A",
+                "start": 283
+            },
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_targets_div_by_zero_bmc/output.json

@@ -1,4 +1,9 @@
-{"auxiliaryInputRequested":{"smtlib2queries":{"0x540d6a4b18ea4181713b8f0e9b4b272f762e142ba1716a3960cfdbed3f1ae64e":"(set-option :produce-models true)
+{
+    "auxiliaryInputRequested":
+    {
+        "smtlib2queries":
+        {
+            "0x540d6a4b18ea4181713b8f0e9b4b272f762e142ba1716a3960cfdbed3f1ae64e": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
 (declare-fun |this_0| () Int)
@@ -55,7 +60,15 @@
 (assert (= |EVALEXPR_2| expr_29_0))
 (check-sat)
 (get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| ))
-"}},"errors":[{"component":"general","errorCode":"3046","formattedMessage":"Warning: BMC: Division by zero happens here.
+"
+        }
+    },
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "3046",
+            "formattedMessage": "Warning: BMC: Division by zero happens here.
   --> A:10:7:
    |
 10 | \t\t\t\t\t\t2 / x;
@@ -68,8 +81,39 @@ Note: Counterexample:
 Note: Callstack:
 Note:
 
-","message":"BMC: Division by zero happens here.","secondarySourceLocations":[{"message":"Counterexample:
+",
+            "message": "BMC: Division by zero happens here.",
+            "secondarySourceLocations":
+            [
+                {
+                    "message": "Counterexample:
   <result> = 0
   a = 0
   x = 0
-"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":216,"file":"A","start":211},"type":"Warning"}],"sources":{"A":{"id":0}}}
+"
+                },
+                {
+                    "message": "Callstack:"
+                },
+                {
+                    "message": ""
+                }
+            ],
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 216,
+                "file": "A",
+                "start": 211
+            },
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_targets_div_by_zero_chc/output.json

@@ -1,4 +1,10 @@
-{"errors":[{"component":"general","errorCode":"4281","formattedMessage":"Warning: CHC: Division by zero happens here.
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "4281",
+            "formattedMessage": "Warning: CHC: Division by zero happens here.
 Counterexample:
 arr = []
 a = 0x0
@@ -13,7 +19,8 @@ test.f(0x0, 1)
 10 | \t\t\t\t\t\t2 / x;
    | \t\t\t\t\t\t^^^^^
 
-","message":"CHC: Division by zero happens here.
+",
+            "message": "CHC: Division by zero happens here.
 Counterexample:
 arr = []
 a = 0x0
@@ -22,4 +29,22 @@ x = 0
 Transaction trace:
 test.constructor()
 State: arr = []
-test.f(0x0, 1)","severity":"warning","sourceLocation":{"end":216,"file":"A","start":211},"type":"Warning"}],"sources":{"A":{"id":0}}}
+test.f(0x0, 1)",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 216,
+                "file": "A",
+                "start": 211
+            },
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_targets_empty_array/output.json

@@ -1 +1,12 @@
-{"errors":[{"component":"general","formattedMessage":"settings.modelChecker.targets must be a non-empty array.","message":"settings.modelChecker.targets must be a non-empty array.","severity":"error","type":"JSONError"}]}
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "formattedMessage": "settings.modelChecker.targets must be a non-empty array.",
+            "message": "settings.modelChecker.targets must be a non-empty array.",
+            "severity": "error",
+            "type": "JSONError"
+        }
+    ]
+}

test/cmdlineTests/standard_model_checker_targets_out_of_bounds_bmc/output.json

@@ -1 +1,9 @@
-{"sources":{"A":{"id":0}}}
+{
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_targets_out_of_bounds_chc/output.json

@@ -1,4 +1,10 @@
-{"errors":[{"component":"general","errorCode":"6368","formattedMessage":"Warning: CHC: Out of bounds access happens here.
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "6368",
+            "formattedMessage": "Warning: CHC: Out of bounds access happens here.
 Counterexample:
 arr = []
 a = 0x0
@@ -13,7 +19,8 @@ test.f(0x0, 1)
 14 | \t\t\t\t\t\tarr[x];
    | \t\t\t\t\t\t^^^^^^
 
-","message":"CHC: Out of bounds access happens here.
+",
+            "message": "CHC: Out of bounds access happens here.
 Counterexample:
 arr = []
 a = 0x0
@@ -22,4 +29,22 @@ x = 0
 Transaction trace:
 test.constructor()
 State: arr = []
-test.f(0x0, 1)","severity":"warning","sourceLocation":{"end":289,"file":"A","start":283},"type":"Warning"}],"sources":{"A":{"id":0}}}
+test.f(0x0, 1)",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 289,
+                "file": "A",
+                "start": 283
+            },
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_targets_overflow_bmc/output.json

@@ -1,4 +1,9 @@
-{"auxiliaryInputRequested":{"smtlib2queries":{"0xb91b28779c6db8b1a6ceecabfa97788476fbb427474cd132376917103e4bc9d9":"(set-option :produce-models true)
+{
+    "auxiliaryInputRequested":
+    {
+        "smtlib2queries":
+        {
+            "0xb91b28779c6db8b1a6ceecabfa97788476fbb427474cd132376917103e4bc9d9": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
 (declare-fun |this_0| () Int)
@@ -55,7 +60,15 @@
 (assert (= |EVALEXPR_2| (+ expr_20_0 expr_25_1)))
 (check-sat)
 (get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| ))
-"}},"errors":[{"component":"general","errorCode":"2661","formattedMessage":"Warning: BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
+"
+        }
+    },
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "2661",
+            "formattedMessage": "Warning: BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
  --> A:9:7:
   |
 9 | \t\t\t\t\t\tx + type(uint).max;
@@ -68,8 +81,39 @@ Note: Counterexample:
 Note: Callstack:
 Note:
 
-","message":"BMC: Overflow (resulting value larger than 2**256 - 1) happens here.","secondarySourceLocations":[{"message":"Counterexample:
+",
+            "message": "BMC: Overflow (resulting value larger than 2**256 - 1) happens here.",
+            "secondarySourceLocations":
+            [
+                {
+                    "message": "Counterexample:
   <result> = 2**256
   a = 0
   x = 1
-"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":203,"file":"A","start":185},"type":"Warning"}],"sources":{"A":{"id":0}}}
+"
+                },
+                {
+                    "message": "Callstack:"
+                },
+                {
+                    "message": ""
+                }
+            ],
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 203,
+                "file": "A",
+                "start": 185
+            },
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_targets_overflow_chc/output.json

@@ -1,4 +1,10 @@
-{"errors":[{"component":"general","errorCode":"4984","formattedMessage":"Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "4984",
+            "formattedMessage": "Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 Counterexample:
 arr = []
 a = 0x0
@@ -13,7 +19,8 @@ test.f(0x0, 2)
 9 | \t\t\t\t\t\tx + type(uint).max;
   | \t\t\t\t\t\t^^^^^^^^^^^^^^^^^^
 
-","message":"CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
+",
+            "message": "CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
 Counterexample:
 arr = []
 a = 0x0
@@ -22,4 +29,22 @@ x = 1
 Transaction trace:
 test.constructor()
 State: arr = []
-test.f(0x0, 2)","severity":"warning","sourceLocation":{"end":203,"file":"A","start":185},"type":"Warning"}],"sources":{"A":{"id":0}}}
+test.f(0x0, 2)",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 203,
+                "file": "A",
+                "start": 185
+            },
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_targets_pop_empty_bmc/output.json

@@ -1 +1,9 @@
-{"sources":{"A":{"id":0}}}
+{
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_targets_pop_empty_chc/output.json

@@ -1,4 +1,10 @@
-{"errors":[{"component":"general","errorCode":"2529","formattedMessage":"Warning: CHC: Empty array \"pop\" happens here.
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "2529",
+            "formattedMessage": "Warning: CHC: Empty array \"pop\" happens here.
 Counterexample:
 arr = []
 a = 0x0
@@ -13,7 +19,8 @@ test.f(0x0, 1)
 13 | \t\t\t\t\t\tarr.pop();
    | \t\t\t\t\t\t^^^^^^^^^
 
-","message":"CHC: Empty array \"pop\" happens here.
+",
+            "message": "CHC: Empty array \"pop\" happens here.
 Counterexample:
 arr = []
 a = 0x0
@@ -22,4 +29,22 @@ x = 0
 Transaction trace:
 test.constructor()
 State: arr = []
-test.f(0x0, 1)","severity":"warning","sourceLocation":{"end":275,"file":"A","start":266},"type":"Warning"}],"sources":{"A":{"id":0}}}
+test.f(0x0, 1)",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 275,
+                "file": "A",
+                "start": 266
+            },
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_targets_underflow_bmc/output.json

@@ -1,4 +1,9 @@
-{"auxiliaryInputRequested":{"smtlib2queries":{"0x6bfae35e234137f12dfe7bc10a8cd34cfa8f3cf1a3439e2e99418358e7bad911":"(set-option :produce-models true)
+{
+    "auxiliaryInputRequested":
+    {
+        "smtlib2queries":
+        {
+            "0x6bfae35e234137f12dfe7bc10a8cd34cfa8f3cf1a3439e2e99418358e7bad911": "(set-option :produce-models true)
 (set-logic ALL)
 (declare-fun |error_0| () Int)
 (declare-fun |this_0| () Int)
@@ -55,7 +60,15 @@
 (assert (= |EVALEXPR_2| (- expr_17_0 1)))
 (check-sat)
 (get-value (|EVALEXPR_0| |EVALEXPR_1| |EVALEXPR_2| ))
-"}},"errors":[{"component":"general","errorCode":"4144","formattedMessage":"Warning: BMC: Underflow (resulting value less than 0) happens here.
+"
+        }
+    },
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "4144",
+            "formattedMessage": "Warning: BMC: Underflow (resulting value less than 0) happens here.
  --> A:8:7:
   |
 8 | \t\t\t\t\t\t--x;
@@ -68,8 +81,39 @@ Note: Counterexample:
 Note: Callstack:
 Note:
 
-","message":"BMC: Underflow (resulting value less than 0) happens here.","secondarySourceLocations":[{"message":"Counterexample:
+",
+            "message": "BMC: Underflow (resulting value less than 0) happens here.",
+            "secondarySourceLocations":
+            [
+                {
+                    "message": "Counterexample:
   <result> = (- 1)
   a = 0
   x = 0
-"},{"message":"Callstack:"},{"message":""}],"severity":"warning","sourceLocation":{"end":177,"file":"A","start":174},"type":"Warning"}],"sources":{"A":{"id":0}}}
+"
+                },
+                {
+                    "message": "Callstack:"
+                },
+                {
+                    "message": ""
+                }
+            ],
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 177,
+                "file": "A",
+                "start": 174
+            },
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}

test/cmdlineTests/standard_model_checker_targets_underflow_chc/output.json

@@ -1,4 +1,10 @@
-{"errors":[{"component":"general","errorCode":"3944","formattedMessage":"Warning: CHC: Underflow (resulting value less than 0) happens here.
+{
+    "errors":
+    [
+        {
+            "component": "general",
+            "errorCode": "3944",
+            "formattedMessage": "Warning: CHC: Underflow (resulting value less than 0) happens here.
 Counterexample:
 arr = []
 a = 0x0
@@ -13,7 +19,8 @@ test.f(0x0, 0)
 8 | \t\t\t\t\t\t--x;
   | \t\t\t\t\t\t^^^
 
-","message":"CHC: Underflow (resulting value less than 0) happens here.
+",
+            "message": "CHC: Underflow (resulting value less than 0) happens here.
 Counterexample:
 arr = []
 a = 0x0
@@ -22,4 +29,22 @@ x = 0
 Transaction trace:
 test.constructor()
 State: arr = []
-test.f(0x0, 0)","severity":"warning","sourceLocation":{"end":177,"file":"A","start":174},"type":"Warning"}],"sources":{"A":{"id":0}}}
+test.f(0x0, 0)",
+            "severity": "warning",
+            "sourceLocation":
+            {
+                "end": 177,
+                "file": "A",
+                "start": 174
+            },
+            "type": "Warning"
+        }
+    ],
+    "sources":
+    {
+        "A":
+        {
+            "id": 0
+        }
+    }
+}