"functions": [
    {
      "instructions": [
        {
          "guard": {
            "id": "constant",
            "named_sub": {
              "type": {
                "id": "bool"
              },
              "value": {
                "id": "false"
              }
            }
          },
          "instruction": "        // 0 file main.c line 3 function main\n        ASSERT FALSE // function main entry point\n",
          "instructionId": "ASSERT",
          "operands": [ ]
        },
        {
          "instruction": "        // 1 file main.c line 3 function main\n        signed int x;\n",
          "instructionId": "DECL",
          "operands": [
            {
              "id": "symbol",
              "named_sub": {
                "identifier": {
                  "id": "main::1::x"
                },
                "type": {
                  "id": "signedbv",
                  "named_sub": {
                    "width": {
                      "id": "32"
                    }
                  }
                }
              }
            }
          ],
          "sourceLocation": {
            "file": "main.c",
            "function": "main",
            "line": "3"
          }
        },
        {
          "instruction": "        // 2 file main.c line 3 function main\n        x = 4;\n",
          "instructionId": "ASSIGN",
          "operands": [
            {
              "id": "symbol",
              "named_sub": {
                "identifier": {
                  "id": "main::1::x"
                },
                "type": {
                  "id": "signedbv",
                  "named_sub": {
                    "width": {
                      "id": "32"
                    }
                  }
                }
              }
            },
            {
              "id": "constant",
              "named_sub": {
                "type": {
                  "id": "signedbv",
                  "named_sub": {
                    "width": {
                      "id": "32"
                    }
                  }
                },
                "value": {
                  "id": "00000000000000000000000000000100"
                }
              }
            }
          ],
          "sourceLocation": {
            "file": "main.c",
            "function": "main",
            "line": "3"
          }
        },
        {
          "instruction": "        // 3 file main.c line 4 function main\n        signed int y;\n",
          "instructionId": "DECL",
          "operands": [
            {
              "id": "symbol",
              "named_sub": {
                "identifier": {
                  "id": "main::1::y"
                },
                "type": {
                  "id": "signedbv",
                  "named_sub": {
                    "width": {
                      "id": "32"
                    }
                  }
                }
              }
            }
          ],
          "sourceLocation": {
            "file": "main.c",
            "function": "main",
            "line": "4"
          }
        },
        {
          "instruction": "        // 4 file main.c line 4 function main\n        y = x * 2;\n",
          "instructionId": "ASSIGN",
          "operands": [
            {
              "id": "symbol",
              "named_sub": {
                "identifier": {
                  "id": "main::1::y"
                },
                "type": {
                  "id": "signedbv",
                  "named_sub": {
                    "width": {
                      "id": "32"
                    }
                  }
                }
              }
            },
            {
              "id": "*",
              "named_sub": {
                "type": {
                  "id": "signedbv",
                  "named_sub": {
                    "width": {
                      "id": "32"
                    }
                  }
                }
              },
              "sub": [
                {
                  "id": "symbol",
                  "named_sub": {
                    "identifier": {
                      "id": "main::1::x"
                    },
                    "type": {
                      "id": "signedbv",
                      "named_sub": {
                        "width": {
                          "id": "32"
                        }
                      }
                    }
                  }
                },
                {
                  "id": "constant",
                  "named_sub": {
                    "type": {
                      "id": "signedbv",
                      "named_sub": {
                        "width": {
                          "id": "32"
                        }
                      }
                    },
                    "value": {
                      "id": "00000000000000000000000000000010"
                    }
                  }
                }
              ]
            }
          ],
          "sourceLocation": {
            "file": "main.c",
            "function": "main",
            "line": "4"
          }
        },
        {
          "instruction": "        // 5 file main.c line 5 function main\n        signed int z;\n",
          "instructionId": "DECL",
          "operands": [
            {
              "id": "symbol",
              "named_sub": {
                "identifier": {
                  "id": "main::1::z"
                },
                "type": {
                  "id": "signedbv",
                  "named_sub": {
                    "width": {
                      "id": "32"
                    }
                  }
                }
              }
            }
          ],
          "sourceLocation": {
            "file": "main.c",
            "function": "main",
            "line": "5"
          }
        },
        {
          "instruction": "        // 6 file main.c line 5 function main\n        z = x + y;\n",
          "instructionId": "ASSIGN",
          "operands": [
            {
              "id": "symbol",
              "named_sub": {
                "identifier": {
                  "id": "main::1::z"
                },
                "type": {
                  "id": "signedbv",
                  "named_sub": {
                    "width": {
                      "id": "32"
                    }
                  }
                }
              }
            },
            {
              "id": "+",
              "named_sub": {
                "type": {
                  "id": "signedbv",
                  "named_sub": {
                    "width": {
                      "id": "32"
                    }
                  }
                }
              },
              "sub": [
                {
                  "id": "symbol",
                  "named_sub": {
                    "identifier": {
                      "id": "main::1::x"
                    },
                    "type": {
                      "id": "signedbv",
                      "named_sub": {
                        "width": {
                          "id": "32"
                        }
                      }
                    }
                  }
                },
                {
                  "id": "symbol",
                  "named_sub": {
                    "identifier": {
                      "id": "main::1::y"
                    },
                    "type": {
                      "id": "signedbv",
                      "named_sub": {
                        "width": {
                          "id": "32"
                        }
                      }
                    }
                  }
                }
              ]
            }
          ],
          "sourceLocation": {
            "file": "main.c",
            "function": "main",
            "line": "5"
          }
        },
        {
          "guard": {
            "id": "not",
            "named_sub": {
              "type": {
                "id": "bool"
              }
            },
            "sub": [
              {
                "id": ">",
                "named_sub": {
                  "type": {
                    "id": "bool"
                  }
                },
                "sub": [
                  {
                    "id": "symbol",
                    "named_sub": {
                      "identifier": {
                        "id": "main::1::x"
                      },
                      "type": {
                        "id": "signedbv",
                        "named_sub": {
                          "width": {
                            "id": "32"
                          }
                        }
                      }
                    }
                  },
                  {
                    "id": "constant",
                    "named_sub": {
                      "type": {
                        "id": "signedbv",
                        "named_sub": {
                          "width": {
                            "id": "32"
                          }
                        }
                      },
                      "value": {
                        "id": "00000000000000000000000000001010"
                      }
                    }
                  }
                ]
              }
            ]
          },
          "instruction": "        // 7 file main.c line 7 function main\n        ASSERT !(x > 10) // function main block 1 branch false\n",
          "instructionId": "ASSERT",
          "operands": [ ]
        },
        {
          "guard": {
            "id": "not",
            "named_sub": {
              "type": {
                "id": "bool"
              }
            },
            "sub": [
              {
                "id": "not",
                "named_sub": {
                  "type": {
                    "id": "bool"
                  }
                },
                "sub": [
                  {
                    "id": ">",
                    "named_sub": {
                      "type": {
                        "id": "bool"
                      }
                    },
                    "sub": [
                      {
                        "id": "symbol",
                        "named_sub": {
                          "identifier": {
                            "id": "main::1::x"
                          },
                          "type": {
                            "id": "signedbv",
                            "named_sub": {
                              "width": {
                                "id": "32"
                              }
                            }
                          }
                        }
                      },
                      {
                        "id": "constant",
                        "named_sub": {
                          "type": {
                            "id": "signedbv",
                            "named_sub": {
                              "width": {
                                "id": "32"
                              }
                            }
                          },
                          "value": {
                            "id": "00000000000000000000000000001010"
                          }
                        }
                      }
                    ]
                  }
                ]
              }
            ]
          },
          "instruction": "        // 8 file main.c line 7 function main\n        ASSERT !(!(x > 10)) // function main block 1 branch true\n",
          "instructionId": "ASSERT",
          "operands": [ ]
        },
        {
          "guard": {
            "id": "not",
            "named_sub": {
              "type": {
                "id": "bool"
              }
            },
            "sub": [
              {
                "id": ">",
                "named_sub": {
                  "type": {
                    "id": "bool"
                  }
                },
                "sub": [
                  {
                    "id": "symbol",
                    "named_sub": {
                      "identifier": {
                        "id": "main::1::x"
                      },
                      "type": {
                        "id": "signedbv",
                        "named_sub": {
                          "width": {
                            "id": "32"
                          }
                        }
                      }
                    }
                  },
                  {
                    "id": "constant",
                    "named_sub": {
                      "type": {
                        "id": "signedbv",
                        "named_sub": {
                          "width": {
                            "id": "32"
                          }
                        }
                      },
                      "value": {
                        "id": "00000000000000000000000000001010"
                      }
                    }
                  }
                ]
              }
            ]
          },
          "instruction": "        // 9 file main.c line 7 function main\n        IF !(x > 10) THEN GOTO 1\n",
          "instructionId": "GOTO",
          "operands": [ ]
        },
        {
          "instruction": "        // 10 file main.c line 9 function main\n        main#return_value = 4;\n",
          "instructionId": "ASSIGN",
          "operands": [
            {
              "id": "symbol",
              "named_sub": {
                "identifier": {
                  "id": "main#return_value"
                },
                "type": {
                  "id": "signedbv",
                  "named_sub": {
                    "width": {
                      "id": "32"
                    }
                  }
                }
              }
            },
            {
              "id": "constant",
              "named_sub": {
                "type": {
                  "id": "signedbv",
                  "named_sub": {
                    "width": {
                      "id": "32"
                    }
                  }
                },
                "value": {
                  "id": "00000000000000000000000000000100"
                }
              }
            }
          ]
        },
        {
          "instruction": "        // 11 file main.c line 9 function main\n        dead z;\n",
          "instructionId": "DEAD",
          "operands": [
            {
              "id": "symbol",
              "named_sub": {
                "identifier": {
                  "id": "main::1::z"
                },
                "type": {
                  "id": "signedbv",
                  "named_sub": {
                    "width": {
                      "id": "32"
                    }
                  }
                }
              }
            }
          ],
          "sourceLocation": {
            "file": "main.c",
            "function": "main",
            "line": "9"
          }
        },
        {
          "instruction": "        // 12 file main.c line 9 function main\n        dead y;\n",
          "instructionId": "DEAD",
          "operands": [
            {
              "id": "symbol",
              "named_sub": {
                "identifier": {
                  "id": "main::1::y"
                },
                "type": {
                  "id": "signedbv",
                  "named_sub": {
                    "width": {
                      "id": "32"
                    }
                  }
                }
              }
            }
          ],
          "sourceLocation": {
            "file": "main.c",
            "function": "main",
            "line": "9"
          }
        },
        {
          "instruction": "        // 13 file main.c line 9 function main\n        dead x;\n",
          "instructionId": "DEAD",
          "operands": [
            {
              "id": "symbol",
              "named_sub": {
                "identifier": {
                  "id": "main::1::x"
                },
                "type": {
                  "id": "signedbv",
                  "named_sub": {
                    "width": {
                      "id": "32"
                    }
                  }
                }
              }
            }
          ],
          "sourceLocation": {
            "file": "main.c",
            "function": "main",
            "line": "9"
          }
        },
        {
          "instruction": "        // 14 file main.c line 9 function main\n        GOTO 2\n",
          "instructionId": "GOTO",
          "operands": [ ]
        },
        {
          "instruction": "        // 15 file main.c line 12 function main\n     1: main#return_value = z;\n",
          "instructionId": "ASSIGN",
          "operands": [
            {
              "id": "symbol",
              "named_sub": {
                "identifier": {
                  "id": "main#return_value"
                },
                "type": {
                  "id": "signedbv",
                  "named_sub": {
                    "width": {
                      "id": "32"
                    }
                  }
                }
              }
            },
            {
              "id": "symbol",
              "named_sub": {
                "identifier": {
                  "id": "main::1::z"
                },
                "type": {
                  "id": "signedbv",
                  "named_sub": {
                    "width": {
                      "id": "32"
                    }
                  }
                }
              }
            }
          ]
        },
        {
          "instruction": "        // 16 file main.c line 12 function main\n        dead z;\n",
          "instructionId": "DEAD",
          "operands": [
            {
              "id": "symbol",
              "named_sub": {
                "identifier": {
                  "id": "main::1::z"
                },
                "type": {
                  "id": "signedbv",
                  "named_sub": {
                    "width": {
                      "id": "32"
                    }
                  }
                }
              }
            }
          ],
          "sourceLocation": {
            "file": "main.c",
            "function": "main",
            "line": "12"
          }
        },
        {
          "instruction": "        // 17 file main.c line 12 function main\n        dead y;\n",
          "instructionId": "DEAD",
          "operands": [
            {
              "id": "symbol",
              "named_sub": {
                "identifier": {
                  "id": "main::1::y"
                },
                "type": {
                  "id": "signedbv",
                  "named_sub": {
                    "width": {
                      "id": "32"
                    }
                  }
                }
              }
            }
          ],
          "sourceLocation": {
            "file": "main.c",
            "function": "main",
            "line": "12"
          }
        },
        {
          "instruction": "        // 18 file main.c line 12 function main\n        dead x;\n",
          "instructionId": "DEAD",
          "operands": [
            {
              "id": "symbol",
              "named_sub": {
                "identifier": {
                  "id": "main::1::x"
                },
                "type": {
                  "id": "signedbv",
                  "named_sub": {
                    "width": {
                      "id": "32"
                    }
                  }
                }
              }
            }
          ],
          "sourceLocation": {
            "file": "main.c",
            "function": "main",
            "line": "12"
          }
        },
        {
          "instruction": "        // 19 file main.c line 13 function main\n     2: END_FUNCTION\n",
          "instructionId": "END_FUNCTION",
          "operands": [ ]
        }
      ],
      "isBodyAvailable": true,
      "isInternal": false,
      "name": "main"
    },
    {
      "instructions": [
        {
          "instruction": "        // 20 no location\n        __CPROVER_initialize();\n",
          "instructionId": "FUNCTION_CALL",
          "operands": [
            {
              "named_sub": {
                "type": {
                  "id": ""
                }
              }
            },
            {
              "id": "symbol",
              "named_sub": {
                "identifier": {
                  "id": "__CPROVER_initialize"
                },
                "type": {
                  "id": "code",
                  "named_sub": {
                    "parameters": {
                      "id": ""
                    },
                    "return_type": {
                      "id": "empty"
                    }
                  }
                }
              }
            },
            {
              "id": "arguments",
              "named_sub": {
                "type": {
                  "id": ""
                }
              }
            }
          ]
        },
        {
          "instruction": "        // 21 file main.c line 1\n        main();\n",
          "instructionId": "FUNCTION_CALL",
          "operands": [
            {
              "named_sub": {
                "type": {
                  "id": ""
                }
              }
            },
            {
              "id": "symbol",
              "named_sub": {
                "identifier": {
                  "id": "main"
                },
                "type": {
                  "id": "code",
                  "named_sub": {
                    "parameters": {
                      "id": "",
                      "named_sub": {
                        "ellipsis": {
                          "id": "1"
                        }
                      }
                    },
                    "return_type": {
                      "id": "empty"
                    }
                  }
                }
              }
            },
            {
              "id": "arguments",
              "named_sub": {
                "type": {
                  "id": ""
                }
              }
            }
          ],
          "sourceLocation": {
            "file": "main.c",
            "line": "1"
          }
        },
        {
          "instruction": "        // 22 file main.c line 1\n        return' = main#return_value;\n",
          "instructionId": "ASSIGN",
          "operands": [
            {
              "id": "symbol",
              "named_sub": {
                "identifier": {
                  "id": "return'"
                },
                "type": {
                  "id": "signedbv",
                  "named_sub": {
                    "width": {
                      "id": "32"
                    }
                  }
                }
              }
            },
            {
              "id": "symbol",
              "named_sub": {
                "identifier": {
                  "id": "main#return_value"
                },
                "type": {
                  "id": "signedbv",
                  "named_sub": {
                    "width": {
                      "id": "32"
                    }
                  }
                }
              }
            }
          ]
        },
        {
          "instruction": "        // 23 file main.c line 1\n        dead main#return_value;\n",
          "instructionId": "DEAD",
          "operands": [
            {
              "id": "symbol",
              "named_sub": {
                "identifier": {
                  "id": "main#return_value"
                },
                "type": {
                  "id": "signedbv",
                  "named_sub": {
                    "width": {
                      "id": "32"
                    }
                  }
                }
              }
            }
          ]
        },
        {
          "instruction": "        // 24 file main.c line 1\n        OUTPUT(\"return\", return');\n",
          "instructionId": "OTHER",
          "operands": [
            {
              "id": "address_of",
              "named_sub": {
                "type": {
                  "id": "pointer",
                  "sub": [
                    {
                      "id": "signedbv",
                      "named_sub": {
                        "width": {
                          "id": "8"
                        }
                      }
                    }
                  ]
                }
              },
              "sub": [
                {
                  "id": "index",
                  "named_sub": {
                    "type": {
                      "id": "signedbv",
                      "named_sub": {
                        "width": {
                          "id": "8"
                        }
                      }
                    }
                  },
                  "sub": [
                    {
                      "id": "string_constant",
                      "named_sub": {
                        "type": {
                          "id": "array",
                          "named_sub": {
                            "size": {
                              "id": "constant",
                              "named_sub": {
                                "type": {
                                  "id": "signedbv",
                                  "named_sub": {
                                    "width": {
                                      "id": "64"
                                    }
                                  }
                                },
                                "value": {
                                  "id": "0000000000000000000000000000000000000000000000000000000000000111"
                                }
                              }
                            }
                          },
                          "sub": [
                            {
                              "id": "signedbv",
                              "named_sub": {
                                "width": {
                                  "id": "8"
                                }
                              }
                            }
                          ]
                        },
                        "value": {
                          "id": "return"
                        }
                      }
                    },
                    {
                      "id": "constant",
                      "named_sub": {
                        "type": {
                          "id": "signedbv",
                          "named_sub": {
                            "width": {
                              "id": "64"
                            }
                          }
                        },
                        "value": {
                          "id": "0000000000000000000000000000000000000000000000000000000000000000"
                        }
                      }
                    }
                  ]
                }
              ]
            },
            {
              "id": "symbol",
              "named_sub": {
                "identifier": {
                  "id": "return'"
                },
                "type": {
                  "id": "signedbv",
                  "named_sub": {
                    "width": {
                      "id": "32"
                    }
                  }
                }
              }
            }
          ],
          "sourceLocation": {
            "file": "main.c",
            "line": "1"
          }
        },
        {
          "instruction": "        // 25 no location\n        END_FUNCTION\n",
          "instructionId": "END_FUNCTION",
          "operands": [ ]
        }
      ],
      "isBodyAvailable": true,
      "isInternal": true,
      "name": "_start"
    },
    {
      "instructions": [
        {
          "instruction": "        // 26 no location\n        // Labels: __CPROVER_HIDE\n        SKIP\n",
          "instructionId": "SKIP",
          "operands": [ ]
        },
        {
          "instruction": "        // 27 file <built-in-additions> line 39\n        __CPROVER_dead_object = NULL;\n",
          "instructionId": "ASSIGN",
          "operands": [
            {
              "id": "symbol",
              "named_sub": {
                "identifier": {
                  "id": "__CPROVER_dead_object"
                },
                "type": {
                  "id": "pointer",
                  "sub": [
                    {
                      "id": "empty"
                    }
                  ]
                }
              }
            },
            {
              "id": "constant",
              "named_sub": {
                "type": {
                  "id": "pointer",
                  "sub": [
                    {
                      "id": "empty"
                    }
                  ]
                },
                "value": {
                  "id": "NULL"
                }
              }
            }
          ],
          "sourceLocation": {
            "file": "<built-in-additions>",
            "line": "39"
          }
        },
        {
          "instruction": "        // 28 file <built-in-additions> line 38\n        __CPROVER_deallocated = NULL;\n",
          "instructionId": "ASSIGN",
          "operands": [
            {
              "id": "symbol",
              "named_sub": {
                "identifier": {
                  "id": "__CPROVER_deallocated"
                },
                "type": {
                  "id": "pointer",
                  "sub": [
                    {
                      "id": "empty"
                    }
                  ]
                }
              }
            },
            {
              "id": "constant",
              "named_sub": {
                "type": {
                  "id": "pointer",
                  "sub": [
                    {
                      "id": "empty"
                    }
                  ]
                },
                "value": {
                  "id": "NULL"
                }
              }
            }
          ],
          "sourceLocation": {
            "file": "<built-in-additions>",
            "line": "38"
          }
        },
        {
          "instruction": "        // 29 file <built-in-additions> line 42\n        __CPROVER_malloc_is_new_array = 0 != 0;\n",
          "instructionId": "ASSIGN",
          "operands": [
            {
              "id": "symbol",
              "named_sub": {
                "identifier": {
                  "id": "__CPROVER_malloc_is_new_array"
                },
                "type": {
                  "id": "bool"
                }
              }
            },
            {
              "id": "notequal",
              "named_sub": {
                "type": {
                  "id": "bool"
                }
              },
              "sub": [
                {
                  "id": "constant",
                  "named_sub": {
                    "type": {
                      "id": "signedbv",
                      "named_sub": {
                        "width": {
                          "id": "32"
                        }
                      }
                    },
                    "value": {
                      "id": "00000000000000000000000000000000"
                    }
                  }
                },
                {
                  "id": "constant",
                  "named_sub": {
                    "type": {
                      "id": "signedbv",
                      "named_sub": {
                        "width": {
                          "id": "32"
                        }
                      }
                    },
                    "value": {
                      "id": "00000000000000000000000000000000"
                    }
                  }
                }
              ]
            }
          ],
          "sourceLocation": {
            "file": "<built-in-additions>",
            "line": "42"
          }
        },
        {
          "instruction": "        // 30 file <built-in-additions> line 40\n        __CPROVER_malloc_object = NULL;\n",
          "instructionId": "ASSIGN",
          "operands": [
            {
              "id": "symbol",
              "named_sub": {
                "identifier": {
                  "id": "__CPROVER_malloc_object"
                },
                "type": {
                  "id": "pointer",
                  "sub": [
                    {
                      "id": "empty"
                    }
                  ]
                }
              }
            },
            {
              "id": "constant",
              "named_sub": {
                "type": {
                  "id": "pointer",
                  "sub": [
                    {
                      "id": "empty"
                    }
                  ]
                },
                "value": {
                  "id": "NULL"
                }
              }
            }
          ],
          "sourceLocation": {
            "file": "<built-in-additions>",
            "line": "40"
          }
        },
        {
          "instruction": "        // 31 file <built-in-additions> line 41\n        __CPROVER_malloc_size = 0ul;\n",
          "instructionId": "ASSIGN",
          "operands": [
            {
              "id": "symbol",
              "named_sub": {
                "identifier": {
                  "id": "__CPROVER_malloc_size"
                },
                "type": {
                  "id": "unsignedbv",
                  "named_sub": {
                    "width": {
                      "id": "64"
                    }
                  }
                }
              }
            },
            {
              "id": "constant",
              "named_sub": {
                "type": {
                  "id": "unsignedbv",
                  "named_sub": {
                    "width": {
                      "id": "64"
                    }
                  }
                },
                "value": {
                  "id": "0000000000000000000000000000000000000000000000000000000000000000"
                }
              }
            }
          ],
          "sourceLocation": {
            "file": "<built-in-additions>",
            "line": "41"
          }
        },
        {
          "instruction": "        // 32 file <built-in-additions> line 43\n        __CPROVER_memory_leak = NULL;\n",
          "instructionId": "ASSIGN",
          "operands": [
            {
              "id": "symbol",
              "named_sub": {
                "identifier": {
                  "id": "__CPROVER_memory_leak"
                },
                "type": {
                  "id": "pointer",
                  "sub": [
                    {
                      "id": "empty"
                    }
                  ]
                }
              }
            },
            {
              "id": "constant",
              "named_sub": {
                "type": {
                  "id": "pointer",
                  "sub": [
                    {
                      "id": "empty"
                    }
                  ]
                },
                "value": {
                  "id": "NULL"
                }
              }
            }
          ],
          "sourceLocation": {
            "file": "<built-in-additions>",
            "line": "43"
          }
        },
        {
          "instruction": "        // 33 file <built-in-additions> line 31\n        __CPROVER_next_thread_id = (unsigned long int)0;\n",
          "instructionId": "ASSIGN",
          "operands": [
            {
              "id": "symbol",
              "named_sub": {
                "identifier": {
                  "id": "__CPROVER_next_thread_id"
                },
                "type": {
                  "id": "unsignedbv",
                  "named_sub": {
                    "width": {
                      "id": "64"
                    }
                  }
                }
              }
            },
            {
              "id": "typecast",
              "named_sub": {
                "type": {
                  "id": "unsignedbv",
                  "named_sub": {
                    "width": {
                      "id": "64"
                    }
                  }
                }
              },
              "sub": [
                {
                  "id": "constant",
                  "named_sub": {
                    "type": {
                      "id": "signedbv",
                      "named_sub": {
                        "width": {
                          "id": "32"
                        }
                      }
                    },
                    "value": {
                      "id": "00000000000000000000000000000000"
                    }
                  }
                }
              ]
            }
          ],
          "sourceLocation": {
            "file": "<built-in-additions>",
            "line": "31"
          }
        },
        {
          "instruction": "        // 34 file <built-in-additions> line 85\n        __CPROVER_pipe_count = (unsigned int)0;\n",
          "instructionId": "ASSIGN",
          "operands": [
            {
              "id": "symbol",
              "named_sub": {
                "identifier": {
                  "id": "__CPROVER_pipe_count"
                },
                "type": {
                  "id": "unsignedbv",
                  "named_sub": {
                    "width": {
                      "id": "32"
                    }
                  }
                }
              }
            },
            {
              "id": "typecast",
              "named_sub": {
                "type": {
                  "id": "unsignedbv",
                  "named_sub": {
                    "width": {
                      "id": "32"
                    }
                  }
                }
              },
              "sub": [
                {
                  "id": "constant",
                  "named_sub": {
                    "type": {
                      "id": "signedbv",
                      "named_sub": {
                        "width": {
                          "id": "32"
                        }
                      }
                    },
                    "value": {
                      "id": "00000000000000000000000000000000"
                    }
                  }
                }
              ]
            }
          ],
          "sourceLocation": {
            "file": "<built-in-additions>",
            "line": "85"
          }
        },
        {
          "instruction": "        // 35 file <built-in-additions> line 65\n        __CPROVER_rounding_mode = 0;\n",
          "instructionId": "ASSIGN",
          "operands": [
            {
              "id": "symbol",
              "named_sub": {
                "identifier": {
                  "id": "__CPROVER_rounding_mode"
                },
                "type": {
                  "id": "signedbv",
                  "named_sub": {
                    "width": {
                      "id": "32"
                    }
                  }
                }
              }
            },
            {
              "id": "constant",
              "named_sub": {
                "type": {
                  "id": "signedbv",
                  "named_sub": {
                    "width": {
                      "id": "32"
                    }
                  }
                },
                "value": {
                  "id": "00000000000000000000000000000000"
                }
              }
            }
          ],
          "sourceLocation": {
            "file": "<built-in-additions>",
            "line": "65"
          }
        },
        {
          "instruction": "        // 36 file <built-in-additions> line 29\n        __CPROVER_thread_id = (unsigned long int)0;\n",
          "instructionId": "ASSIGN",
          "operands": [
            {
              "id": "symbol",
              "named_sub": {
                "identifier": {
                  "id": "__CPROVER_thread_id"
                },
                "type": {
                  "id": "unsignedbv",
                  "named_sub": {
                    "width": {
                      "id": "64"
                    }
                  }
                }
              }
            },
            {
              "id": "typecast",
              "named_sub": {
                "type": {
                  "id": "unsignedbv",
                  "named_sub": {
                    "width": {
                      "id": "64"
                    }
                  }
                }
              },
              "sub": [
                {
                  "id": "constant",
                  "named_sub": {
                    "type": {
                      "id": "signedbv",
                      "named_sub": {
                        "width": {
                          "id": "32"
                        }
                      }
                    },
                    "value": {
                      "id": "00000000000000000000000000000000"
                    }
                  }
                }
              ]
            }
          ],
          "sourceLocation": {
            "file": "<built-in-additions>",
            "line": "29"
          }
        },
        {
          "instruction": "        // 37 file <built-in-additions> line 30\n        __CPROVER_threads_exited = ARRAY_OF(FALSE);\n",
          "instructionId": "ASSIGN",
          "operands": [
            {
              "id": "symbol",
              "named_sub": {
                "identifier": {
                  "id": "__CPROVER_threads_exited"
                },
                "type": {
                  "id": "array",
                  "named_sub": {
                    "size": {
                      "id": "infinity",
                      "named_sub": {
                        "type": {
                          "id": "signedbv",
                          "named_sub": {
                            "width": {
                              "id": "64"
                            }
                          }
                        }
                      }
                    }
                  },
                  "sub": [
                    {
                      "id": "bool"
                    }
                  ]
                }
              }
            },
            {
              "id": "array_of",
              "named_sub": {
                "type": {
                  "id": "array",
                  "named_sub": {
                    "size": {
                      "id": "infinity",
                      "named_sub": {
                        "type": {
                          "id": "signedbv",
                          "named_sub": {
                            "width": {
                              "id": "64"
                            }
                          }
                        }
                      }
                    }
                  },
                  "sub": [
                    {
                      "id": "bool"
                    }
                  ]
                }
              },
              "sub": [
                {
                  "id": "constant",
                  "named_sub": {
                    "type": {
                      "id": "bool"
                    },
                    "value": {
                      "id": "false"
                    }
                  }
                }
              ]
            }
          ],
          "sourceLocation": {
            "file": "<built-in-additions>",
            "line": "30"
          }
        },
        {
          "instruction": "        // 38 no location\n        END_FUNCTION\n",
          "instructionId": "END_FUNCTION",
          "operands": [ ]
        }
      ],
      "isBodyAvailable": true,
      "isInternal": true,
      "name": "__CPROVER_initialize"
    }
  ]