| <?xml version="1.0" encoding="UTF-8" standalone="no"?> |
| <!-- Creator: fig2dev Version 3.2 Patchlevel 5e --> |
| |
| <!-- CreationDate: Tue Aug 22 20:34:06 2017 --> |
| |
| <!-- Magnification: 1.000 --> |
| |
| <svg |
| xmlns:dc="http://purl.org/dc/elements/1.1/" |
| xmlns:cc="http://creativecommons.org/ns#" |
| xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#" |
| xmlns:svg="http://www.w3.org/2000/svg" |
| xmlns="http://www.w3.org/2000/svg" |
| xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd" |
| xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape" |
| width="201.15463" |
| height="310.99545" |
| viewBox="-12 -12 2699.9421 4142.6196" |
| id="svg2" |
| version="1.1" |
| inkscape:version="0.48.4 r9939" |
| sodipodi:docname="cbmc.svg"> |
| <metadata |
| id="metadata160"> |
| <rdf:RDF> |
| <cc:Work |
| rdf:about=""> |
| <dc:format>image/svg+xml</dc:format> |
| <dc:type |
| rdf:resource="http://purl.org/dc/dcmitype/StillImage" /> |
| <dc:title /> |
| </cc:Work> |
| </rdf:RDF> |
| </metadata> |
| <defs |
| id="defs158"> |
| <marker |
| inkscape:stockid="Arrow1Mend" |
| orient="auto" |
| refY="0" |
| refX="0" |
| id="Arrow1Mend" |
| style="overflow:visible"> |
| <path |
| id="path3935" |
| d="M 0,0 5,-5 -12.5,0 5,5 0,0 z" |
| style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt" |
| transform="matrix(-0.4,0,0,-0.4,-4,0)" |
| inkscape:connector-curvature="0" /> |
| </marker> |
| <marker |
| inkscape:stockid="Arrow1Mstart" |
| orient="auto" |
| refY="0" |
| refX="0" |
| id="Arrow1Mstart" |
| style="overflow:visible"> |
| <path |
| id="path3932" |
| d="M 0,0 5,-5 -12.5,0 5,5 0,0 z" |
| style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt" |
| transform="matrix(0.4,0,0,0.4,4,0)" |
| inkscape:connector-curvature="0" /> |
| </marker> |
| <marker |
| inkscape:stockid="Arrow2Lstart" |
| orient="auto" |
| refY="0" |
| refX="0" |
| id="Arrow2Lstart" |
| style="overflow:visible"> |
| <path |
| id="path3944" |
| style="fill-rule:evenodd;stroke-width:0.625;stroke-linejoin:round" |
| d="M 8.7185878,4.0337352 -2.2072895,0.01601326 8.7185884,-4.0017078 c -1.7454984,2.3720609 -1.7354408,5.6174519 -6e-7,8.035443 z" |
| transform="matrix(1.1,0,0,1.1,1.1,0)" |
| inkscape:connector-curvature="0" /> |
| </marker> |
| <marker |
| inkscape:stockid="Arrow1Mstart" |
| orient="auto" |
| refY="0" |
| refX="0" |
| id="Arrow1Mstart-3" |
| style="overflow:visible"> |
| <path |
| inkscape:connector-curvature="0" |
| id="path3932-6" |
| d="M 0,0 5,-5 -12.5,0 5,5 0,0 z" |
| style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt" |
| transform="matrix(0.4,0,0,0.4,4,0)" /> |
| </marker> |
| <marker |
| inkscape:stockid="Arrow1Mend" |
| orient="auto" |
| refY="0" |
| refX="0" |
| id="Arrow1Mend-7" |
| style="overflow:visible"> |
| <path |
| inkscape:connector-curvature="0" |
| id="path3935-5" |
| d="M 0,0 5,-5 -12.5,0 5,5 0,0 z" |
| style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt" |
| transform="matrix(-0.4,0,0,-0.4,-4,0)" /> |
| </marker> |
| <marker |
| inkscape:stockid="Arrow1Mstart" |
| orient="auto" |
| refY="0" |
| refX="0" |
| id="Arrow1Mstart-5" |
| style="overflow:visible"> |
| <path |
| inkscape:connector-curvature="0" |
| id="path3932-62" |
| d="M 0,0 5,-5 -12.5,0 5,5 0,0 z" |
| style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt" |
| transform="matrix(0.4,0,0,0.4,4,0)" /> |
| </marker> |
| <marker |
| inkscape:stockid="Arrow1Mend" |
| orient="auto" |
| refY="0" |
| refX="0" |
| id="Arrow1Mend-9" |
| style="overflow:visible"> |
| <path |
| inkscape:connector-curvature="0" |
| id="path3935-1" |
| d="M 0,0 5,-5 -12.5,0 5,5 0,0 z" |
| style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt" |
| transform="matrix(-0.4,0,0,-0.4,-4,0)" /> |
| </marker> |
| <marker |
| inkscape:stockid="Arrow1Mstart" |
| orient="auto" |
| refY="0" |
| refX="0" |
| id="marker4968" |
| style="overflow:visible"> |
| <path |
| inkscape:connector-curvature="0" |
| id="path4970" |
| d="M 0,0 5,-5 -12.5,0 5,5 0,0 z" |
| style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt" |
| transform="matrix(0.4,0,0,0.4,4,0)" /> |
| </marker> |
| <marker |
| inkscape:stockid="Arrow1Mend" |
| orient="auto" |
| refY="0" |
| refX="0" |
| id="marker4972" |
| style="overflow:visible"> |
| <path |
| inkscape:connector-curvature="0" |
| id="path4974" |
| d="M 0,0 5,-5 -12.5,0 5,5 0,0 z" |
| style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt" |
| transform="matrix(-0.4,0,0,-0.4,-4,0)" /> |
| </marker> |
| <marker |
| inkscape:stockid="Arrow1Mstart" |
| orient="auto" |
| refY="0" |
| refX="0" |
| id="Arrow1Mstart-0" |
| style="overflow:visible"> |
| <path |
| inkscape:connector-curvature="0" |
| id="path3932-9" |
| d="M 0,0 5,-5 -12.5,0 5,5 0,0 z" |
| style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt" |
| transform="matrix(0.4,0,0,0.4,4,0)" /> |
| </marker> |
| <marker |
| inkscape:stockid="Arrow1Mend" |
| orient="auto" |
| refY="0" |
| refX="0" |
| id="Arrow1Mend-3" |
| style="overflow:visible"> |
| <path |
| inkscape:connector-curvature="0" |
| id="path3935-6" |
| d="M 0,0 5,-5 -12.5,0 5,5 0,0 z" |
| style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt" |
| transform="matrix(-0.4,0,0,-0.4,-4,0)" /> |
| </marker> |
| <marker |
| inkscape:stockid="Arrow1Mstart" |
| orient="auto" |
| refY="0" |
| refX="0" |
| id="Arrow1Mstart-6" |
| style="overflow:visible"> |
| <path |
| inkscape:connector-curvature="0" |
| id="path3932-2" |
| d="M 0,0 5,-5 -12.5,0 5,5 0,0 z" |
| style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt" |
| transform="matrix(0.4,0,0,0.4,4,0)" /> |
| </marker> |
| <marker |
| inkscape:stockid="Arrow1Mend" |
| orient="auto" |
| refY="0" |
| refX="0" |
| id="Arrow1Mend-6" |
| style="overflow:visible"> |
| <path |
| inkscape:connector-curvature="0" |
| id="path3935-18" |
| d="M 0,0 5,-5 -12.5,0 5,5 0,0 z" |
| style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt" |
| transform="matrix(-0.4,0,0,-0.4,-4,0)" /> |
| </marker> |
| <marker |
| inkscape:stockid="Arrow1Mstart" |
| orient="auto" |
| refY="0" |
| refX="0" |
| id="Arrow1Mstart-9" |
| style="overflow:visible"> |
| <path |
| id="path3932-27" |
| d="M 0,0 5,-5 -12.5,0 5,5 0,0 z" |
| style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt" |
| transform="matrix(0.4,0,0,0.4,4,0)" |
| inkscape:connector-curvature="0" /> |
| </marker> |
| <marker |
| inkscape:stockid="Arrow1Mend" |
| orient="auto" |
| refY="0" |
| refX="0" |
| id="Arrow1Mend-4" |
| style="overflow:visible"> |
| <path |
| id="path3935-2" |
| d="M 0,0 5,-5 -12.5,0 5,5 0,0 z" |
| style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt" |
| transform="matrix(-0.4,0,0,-0.4,-4,0)" |
| inkscape:connector-curvature="0" /> |
| </marker> |
| <marker |
| inkscape:stockid="Arrow1Mend" |
| orient="auto" |
| refY="0" |
| refX="0" |
| id="Arrow1Mend-2" |
| style="overflow:visible"> |
| <path |
| id="path3935-9" |
| d="M 0,0 5,-5 -12.5,0 5,5 0,0 z" |
| style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt" |
| transform="matrix(-0.4,0,0,-0.4,-4,0)" |
| inkscape:connector-curvature="0" /> |
| </marker> |
| <marker |
| inkscape:stockid="Arrow1Mend" |
| orient="auto" |
| refY="0" |
| refX="0" |
| id="Arrow1Mend-27" |
| style="overflow:visible"> |
| <path |
| id="path3935-0" |
| d="M 0,0 5,-5 -12.5,0 5,5 0,0 z" |
| style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt" |
| transform="matrix(-0.4,0,0,-0.4,-4,0)" |
| inkscape:connector-curvature="0" /> |
| </marker> |
| <marker |
| inkscape:stockid="Arrow1Mend" |
| orient="auto" |
| refY="0" |
| refX="0" |
| id="Arrow1Mend-8" |
| style="overflow:visible"> |
| <path |
| id="path3935-7" |
| d="M 0,0 5,-5 -12.5,0 5,5 0,0 z" |
| style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt" |
| transform="matrix(-0.4,0,0,-0.4,-4,0)" |
| inkscape:connector-curvature="0" /> |
| </marker> |
| <marker |
| inkscape:stockid="Arrow1Mend" |
| orient="auto" |
| refY="0" |
| refX="0" |
| id="Arrow1Mend-92" |
| style="overflow:visible"> |
| <path |
| id="path3935-28" |
| d="M 0,0 5,-5 -12.5,0 5,5 0,0 z" |
| style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt" |
| transform="matrix(-0.4,0,0,-0.4,-4,0)" |
| inkscape:connector-curvature="0" /> |
| </marker> |
| <marker |
| inkscape:stockid="Arrow1Mend" |
| orient="auto" |
| refY="0" |
| refX="0" |
| id="Arrow1Mend-36" |
| style="overflow:visible"> |
| <path |
| id="path3935-75" |
| d="M 0,0 5,-5 -12.5,0 5,5 0,0 z" |
| style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt" |
| transform="matrix(-0.4,0,0,-0.4,-4,0)" |
| inkscape:connector-curvature="0" /> |
| </marker> |
| <marker |
| inkscape:stockid="Arrow1Mend" |
| orient="auto" |
| refY="0" |
| refX="0" |
| id="Arrow1Mend-5" |
| style="overflow:visible"> |
| <path |
| id="path3935-62" |
| d="M 0,0 5,-5 -12.5,0 5,5 0,0 z" |
| style="fill-rule:evenodd;stroke:#000000;stroke-width:1pt" |
| transform="matrix(-0.4,0,0,-0.4,-4,0)" |
| inkscape:connector-curvature="0" /> |
| </marker> |
| </defs> |
| <sodipodi:namedview |
| pagecolor="#ffffff" |
| bordercolor="#666666" |
| borderopacity="1" |
| objecttolerance="10" |
| gridtolerance="10" |
| guidetolerance="10" |
| inkscape:pageopacity="0" |
| inkscape:pageshadow="2" |
| inkscape:window-width="1321" |
| inkscape:window-height="995" |
| id="namedview156" |
| showgrid="true" |
| inkscape:zoom="2.885542" |
| inkscape:cx="81.402868" |
| inkscape:cy="157.29819" |
| inkscape:window-x="599" |
| inkscape:window-y="177" |
| inkscape:window-maximized="0" |
| inkscape:current-layer="svg2" |
| fit-margin-top="5" |
| fit-margin-right="5" |
| fit-margin-bottom="5" |
| fit-margin-left="5" |
| inkscape:snap-global="false" |
| showguides="false"> |
| <inkscape:grid |
| type="xygrid" |
| id="grid3110" |
| empspacing="5" |
| visible="true" |
| enabled="true" |
| snapvisiblegridlinesonly="true" |
| originx="-124.80481px" |
| originy="85.51791px" /> |
| </sodipodi:namedview> |
| <rect |
| id="rect8" |
| style="fill:none;stroke:#000000;stroke-width:7;stroke-linecap:butt;stroke-linejoin:miter" |
| rx="0" |
| height="532.82019" |
| width="1473.3256" |
| y="48.39402" |
| x="188.25179" |
| ry="0" /> |
| <text |
| style="font-size:108px;font-style:normal;font-weight:normal;text-anchor:middle;fill:#000000;stroke-width:0.025in;font-family:Helvetica" |
| id="text106" |
| font-size="108" |
| font-weight="normal" |
| font-style="normal" |
| y="363.72809" |
| x="924.62189" |
| xml:space="preserve"><tspan |
| id="tspan3035" |
| style="font-size:134.222229px">C Code</tspan></text> |
| <text |
| style="font-size:107.99999237px;font-style:normal;font-weight:normal;text-anchor:middle;fill:#000000;stroke-width:0.025in;font-family:Helvetica" |
| id="text106-6" |
| font-size="108" |
| font-weight="normal" |
| font-style="normal" |
| y="1228.2394" |
| x="927.01105" |
| xml:space="preserve"><tspan |
| id="tspan3035-7" |
| style="font-size:134.22221375px">Logic Expression</tspan></text> |
| <rect |
| id="rect8-5" |
| style="fill:none;stroke:#000000;stroke-width:6.99999952;stroke-linecap:butt;stroke-linejoin:miter" |
| rx="0" |
| height="532.82019" |
| width="1473.3254" |
| y="927.53558" |
| x="191.04366" |
| ry="0" /> |
| <text |
| style="font-size:107.99999237px;font-style:normal;font-weight:normal;text-anchor:middle;fill:#000000;stroke-width:0.025in;font-family:Helvetica" |
| id="text106-6-3" |
| font-size="108" |
| font-weight="normal" |
| font-style="normal" |
| y="2102.8625" |
| x="920.63434" |
| xml:space="preserve"><tspan |
| id="tspan3035-7-5" |
| style="font-size:134.22219849px">SAT Solver</tspan></text> |
| <rect |
| id="rect8-5-6" |
| style="fill:none;stroke:#000000;stroke-width:6.99999905;stroke-linecap:butt;stroke-linejoin:miter" |
| rx="0" |
| height="532.82019" |
| width="1473.3253" |
| y="1802.1581" |
| x="191.24532" |
| ry="0" /> |
| <path |
| inkscape:connector-curvature="0" |
| id="path4548-3-1" |
| d="m 928.21412,1456.3291 -0.6701,332.2642" |
| style="fill:none;stroke:#000000;stroke-width:13.42222214px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-start:none;marker-end:url(#Arrow1Mend)" |
| sodipodi:nodetypes="cc" /> |
| <flowRoot |
| xml:space="preserve" |
| id="flowRoot3180" |
| style="font-size:16px;font-style:normal;font-weight:normal;text-align:center;line-height:125%;letter-spacing:0px;word-spacing:0px;text-anchor:middle;fill:#000000;fill-opacity:1;stroke:none;font-family:Sans" |
| transform="matrix(13.422222,0,0,13.422222,-1687.1578,691.81255)"><flowRegion |
| id="flowRegion3182"><rect |
| id="rect3184" |
| width="150.70676" |
| height="74.005592" |
| x="117.62479" |
| y="54.273159" /></flowRegion><flowPara |
| id="flowPara3186" /></flowRoot> <text |
| style="font-size:107.99999237px;font-style:normal;font-weight:normal;text-anchor:middle;fill:#000000;stroke-width:0.025in;font-family:Helvetica" |
| id="text106-6-3-9" |
| font-size="108" |
| font-weight="normal" |
| font-style="normal" |
| y="2979.5476" |
| x="929.02496" |
| xml:space="preserve"><tspan |
| style="font-size:134.22221375px" |
| id="tspan3267">(If Counterexample</tspan></text> |
| <rect |
| id="rect8-5-6-6" |
| style="fill:none;stroke:#000000;stroke-width:6.99999905;stroke-linecap:butt;stroke-linejoin:miter" |
| rx="0" |
| height="532.82019" |
| width="1473.3253" |
| y="2676.9353" |
| x="194.33272" |
| ry="0" /> |
| <path |
| inkscape:connector-curvature="0" |
| id="path4548-3-1-0" |
| d="m 931.30162,2331.1063 -0.6701,332.2641" |
| style="fill:none;stroke:#000000;stroke-width:13.42222214px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-start:none;marker-end:url(#Arrow1Mend)" |
| sodipodi:nodetypes="cc" /> |
| <text |
| style="font-size:107.99999237px;font-style:normal;font-weight:normal;text-anchor:middle;fill:#000000;stroke-width:0.025in;font-family:Helvetica" |
| id="text106-6-3-9-6" |
| font-size="108" |
| font-weight="normal" |
| font-style="normal" |
| y="2817.2178" |
| x="934.25958" |
| xml:space="preserve"><tspan |
| id="tspan3035-7-5-3-2" |
| style="font-size:134.22219849px">Trace Generation</tspan><tspan |
| style="font-size:134.22219849px" |
| id="tspan3223-6" /></text> |
| <text |
| style="font-size:107.99999237px;font-style:normal;font-weight:normal;text-anchor:middle;fill:#000000;stroke-width:0.025in;font-family:Helvetica" |
| id="text106-6-3-9-1" |
| font-size="108" |
| font-weight="normal" |
| font-style="normal" |
| y="3139.4614" |
| x="930.86017" |
| xml:space="preserve"><tspan |
| style="font-size:134.22221375px" |
| id="tspan3269">Located)</tspan></text> |
| <rect |
| id="rect8-2" |
| style="fill:none;stroke:#000000;stroke-width:6.99999952;stroke-linecap:butt;stroke-linejoin:miter" |
| rx="0" |
| height="532.82019" |
| width="1473.3254" |
| y="3548.6016" |
| x="194.998" |
| ry="0" /> |
| <text |
| style="font-size:107.99999237px;font-style:normal;font-weight:normal;text-anchor:middle;fill:#000000;stroke-width:0.025in;font-family:Helvetica" |
| id="text106-0" |
| font-size="108" |
| font-weight="normal" |
| font-style="normal" |
| y="3863.9355" |
| x="931.36798" |
| xml:space="preserve"><tspan |
| id="tspan3035-2" |
| style="font-size:134.22221375px">Verification Result</tspan></text> |
| <rect |
| style="fill:none;stroke:#000000;stroke-width:13.42222214;stroke-miterlimit:1;stroke-opacity:1;stroke-dasharray:26.84444346, 13.42222173;stroke-dashoffset:0" |
| id="rect3319" |
| width="1739.6769" |
| height="2549.0454" |
| x="61.82222" |
| y="796.16034" /> |
| <text |
| style="font-size:107.99999237px;font-style:normal;font-weight:normal;text-anchor:middle;fill:#000000;stroke-width:0.025in;font-family:Helvetica" |
| id="text106-3" |
| font-size="108" |
| font-weight="normal" |
| font-style="normal" |
| y="960.77002" |
| x="2429.1648" |
| xml:space="preserve"><tspan |
| id="tspan3035-75" |
| style="font-size:134.22221375px">CBMC</tspan></text> |
| <path |
| inkscape:connector-curvature="0" |
| id="path4548-3-97" |
| d="M 2216.4281,962.50535 1832.3547,1084.1156" |
| style="fill:none;stroke:#000000;stroke-width:13.42222214px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-start:none;marker-end:url(#Arrow1Mend)" |
| sodipodi:nodetypes="cc" /> |
| <path |
| inkscape:connector-curvature="0" |
| id="path4548-3-1-3" |
| d="m 936.81992,577.87668 -0.6701,332.26411" |
| style="fill:none;stroke:#000000;stroke-width:13.42222214px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-start:none;marker-end:url(#Arrow1Mend)" |
| sodipodi:nodetypes="cc" /> |
| <path |
| inkscape:connector-curvature="0" |
| id="path4548-3-1-0-9" |
| d="m 936.81992,3210.6499 -0.6701,332.2641" |
| style="fill:none;stroke:#000000;stroke-width:13.42222214px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-start:none;marker-end:url(#Arrow1Mend)" |
| sodipodi:nodetypes="cc" /> |
| </svg> |
