diagram/solving.svg

<svg xmlns="http://www.w3.org/2000/svg" xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape" xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd" xmlns:xlink="http://www.w3.org/1999/xlink" id="svg2" width="995" height="975" inkscape:version="0.48.3.1 r9886" sodipodi:docname="solving.svg">
  <sodipodi:namedview id="namedview4" bordercolor="#aeaeae" borderopacity="1" fit-margin-bottom="0" fit-margin-left="0" fit-margin-right="0" fit-margin-top="0" pagecolor="#ffffff" showborder="true" showgrid="true" showguides="false" inkscape:bbox-nodes="false" inkscape:current-layer="g420" inkscape:cx="686.256" inkscape:cy="442.591" inkscape:document-units="px" inkscape:guide-bbox="true" inkscape:object-nodes="true" inkscape:object-paths="true" inkscape:pageopacity="1" inkscape:pageshadow="2" inkscape:showpageshadow="false" inkscape:snap-bbox="true" inkscape:snap-center="false" inkscape:snap-global="true" inkscape:snap-intersection-paths="true" inkscape:snap-nodes="true" inkscape:snap-page="true" inkscape:snap-smooth-nodes="true" inkscape:snap-text-baseline="true" inkscape:window-height="1091" inkscape:window-maximized="0" inkscape:window-width="1115" inkscape:window-x="730" inkscape:window-y="53" inkscape:zoom="1">
    <inkscape:grid id="grid6" color="#9bc2cd" empcolor="#abc7d1" empopacity=".251" empspacing="5" enabled="true" opacity=".125" originx="-915" originy="555" snapvisiblegridlinesonly="true" type="xygrid" visible="true"/>
    <sodipodi:guide id="guide8" orientation="0,1" position="14.999998,705"/>
    <sodipodi:guide id="guide10" orientation="0,1" position="14.999998,735"/>
    <sodipodi:guide id="guide12" orientation="0,1" position="14.999998,765"/>
    <sodipodi:guide id="guide14" orientation="0,1" position="14.999998,795"/>
    <sodipodi:guide id="guide16" orientation="0,1" position="14.999998,655"/>
    <sodipodi:guide id="guide18" orientation="0,1" position="14.999998,605"/>
    <sodipodi:guide id="guide20" orientation="0,1" position="14.999998,555"/>
    <sodipodi:guide id="guide22" orientation="0,1" position="14.999998,505"/>
    <sodipodi:guide id="guide24" orientation="0,1" position="14.999998,455"/>
    <sodipodi:guide id="guide26" orientation="0,1" position="14.999998,405"/>
    <sodipodi:guide id="guide28" orientation="0,1" position="14.999998,365"/>
    <sodipodi:guide id="guide30" orientation="0,1" position="14.999998,315"/>
    <sodipodi:guide id="guide32" orientation="0,1" position="14.999998,215"/>
    <sodipodi:guide id="guide34" orientation="0,1" position="14.999998,265"/>
    <sodipodi:guide id="guide38" orientation="0,1" position="14.999998,165"/>
    <sodipodi:guide id="guide40" orientation="0,1" position="14.999998,115"/>
    <sodipodi:guide id="guide42" orientation="0,1" position="14.999998,65"/>
    <sodipodi:guide id="guide44" orientation="0,1" position="14.999998,815"/>
    <sodipodi:guide id="guide46" orientation="0,1" position="14.999998,825"/>
    <sodipodi:guide id="guide48" orientation="0,1" position="14.999998,835"/>
    <sodipodi:guide id="guide50" orientation="0,1" position="14.999998,845"/>
    <sodipodi:guide id="guide52" orientation="0,1" position="14.999998,855"/>
    <sodipodi:guide id="guide54" orientation="0,1" position="14.999998,865"/>
    <sodipodi:guide id="guide3490" orientation="0,1" position="14.999998,875"/>
    <sodipodi:guide id="guide3492" orientation="0,1" position="14.999998,885"/>
    <sodipodi:guide id="guide3494" orientation="0,1" position="14.999998,895"/>
    <sodipodi:guide id="guide3496" orientation="0,1" position="14.999998,905"/>
    <sodipodi:guide id="guide3498" orientation="0,1" position="14.999998,915"/>
    <sodipodi:guide id="guide3500" orientation="0,1" position="14.999998,925"/>
    <sodipodi:guide id="guide3502" orientation="0,1" position="14.999998,935"/>
    <sodipodi:guide id="guide3504" orientation="0,1" position="14.999998,945"/>
    <sodipodi:guide id="guide3506" orientation="0,1" position="14.999998,955"/>
  </sodipodi:namedview>
  <g id="g64" fill="#816647" fill-opacity=".498" transform="translate(-915 -620)" inkscape:groupmode="layer" inkscape:label="group">
    <path id="path74" d="M1468.572 1035c6.857 0 11.428 3.843 11.428 9.608v305.784c0 5.765-4.572 9.608-11.428 9.608h-57.143c-6.858 0-11.429-3.843-11.429-9.608v-305.784c0-5.765 4.572-9.608 11.428-9.608z" opacity=".14" inkscape:connector-curvature="0" sodipodi:nodetypes="cccsscccc"/>
    <rect id="rect3573" width="80" height="300" x="1120" y="1265" opacity=".14" rx="10" ry="8.243"/>
    <path id="path66" d="M1640 1130v220c0 6-4 10-9 10h-231c-6 0-10-4-10-10v-65c0-6 4-10 10-10h80c6 0 10-4 10-10v-135c0-6 4-10 10-10h130c6 0 10 4 10 10z" opacity=".14" inkscape:connector-curvature="0" sodipodi:nodetypes="ccccccccccccc"/>
    <rect id="rect70" width="80" height="440" x="1120" y="725" opacity=".14" rx="5.833" ry="7.416"/>
    <rect id="rect4168" width="160" height="290" x="1120" y="1275" opacity=".14" rx="10" ry="8.243"/>
    <path id="rect12936" d="M1020 1010h70c6 0 10-4 10-10V895c0-6 4-10 10-10h90c5.54 0 10 4.46 10 10v60c0 6-4 10-10 10h-80c-6 0-10 4-10 10v505c0 6-4 10-10 10h-80c-5.54 0-10-4.46-10-10v-460c0-5.54 4.46-10 10-10z" opacity=".14" inkscape:connector-curvature="0" sodipodi:nodetypes="sccccsscccccccsss"/>
    <rect id="rect6060" width="150" height="380" x="1730" y="790" opacity=".14" rx="10" ry="10"/>
    <path id="rect6062" d="M1660 1085h150c5.54 0 10 4.46 10 10v55c0 5.54-4.46 10-10 10h-70c-6 0-10 4-10 10v290c0 6-4 10-10 10h-60c-5.54 0-10-4.46-10-10v-365c0-5.54 4.46-10 10-10z" opacity=".14" inkscape:connector-curvature="0" sodipodi:nodetypes="sssssccccssss"/>
    <rect id="rect13575" width="150" height="95" x="1430" y="775" opacity=".14" rx="10" ry="10"/>
    <path id="path13808" d="M990 1480c0 6 4 10 10 10h80c6 0 10-4 10-10v-45c0-6-4-10-10-10h-70c-6 0-10-4-10-10v-190c0-6 4-10 10-10h70c6 0 10-4 10-10V930c0-6-4-10-10-10h-80c-6 0-10 4-10 10z" opacity=".14" inkscape:connector-curvature="0" sodipodi:nodetypes="ccccccccccccccccc"/>
    <rect id="rect3575" width="170" height="100" x="1120" y="1465" opacity=".14" rx="10" ry="8.243"/>
    <rect id="rect3653" width="80" height="205" x="1300" y="1325" opacity=".14" rx="10" ry="10"/>
  </g>
  <g id="g96" stroke-width=".7" transform="translate(-915 -620)" inkscape:groupmode="layer" inkscape:label="box">
    <rect id="rect152" width="60" height="45" x="1740" y="1235" fill="#c8daa4" rx="2" ry="2"/>
    <rect id="rect168" width="60" height="30" x="1130" y="995" fill="#c8daa4" rx="2" ry="2"/>
    <a id="box_z3" transform="matrix(1.99983 0 0 1.60004 -1439.757 -243.033)" xlink:href="http://dl.acm.org/citation.cfm?id=1792766" xlink:title="Z3: an efficient SMT solver">
      <rect id="rect260" width="30" height="25" x="1425" y="805" fill="#c8daa4" rx="1" ry="1.25"/>
    </a>
    <rect id="rect264" width="60" height="40" x="1740" y="835" fill="#adc57d" rx="2" ry="2"/>
    <rect id="rect268" width="30" height="10" x="1130" y="1027.5" fill="#adc57d" rx="1" ry="1"/>
    <rect id="rect278" width="60" height="35" x="1740" y="1385" fill="#c8daa4" rx="2" ry="2"/>
    <rect id="rect290" width="60" height="30" x="1410" y="1285" fill="#c8daa4" rx="2" ry="2"/>
    <rect id="rect326" width="10" height="10" x="1830" y="665" fill="#adc57d" rx="2" ry="2"/>
    <rect id="rect4851" width="10" height="10" x="1830" y="650" fill="#c8daa4" rx="2" ry="2"/>
    <rect id="rect4111" width="60" height="30" x="1500" y="1285" fill="#c8daa4" rx="2" ry="2"/>
    <rect id="rect4127" width="60" height="30" x="1130" y="1285" fill="#c8daa4" rx="2" ry="2"/>
    <rect id="rect4191" width="20" height="10" x="1130" y="1317.5" fill="#c8daa4" rx="1" ry="1"/>
    <rect id="rect4967" width="60" height="30" x="1130" y="1485" fill="#c8daa4" rx="2" ry="2"/>
    <rect id="rect4975" width="20" height="10" x="1130" y="1517.5" fill="#c8daa4" rx="1" ry="1"/>
    <rect id="rect5025" width="40" height="40" x="1500" y="1145" fill="#e4d3c2" rx="2" ry="2"/>
    <rect id="rect5082" width="40" height="40" x="1542.5" y="1145" fill="#c8daa4" rx="2" ry="2"/>
    <rect id="rect4221" width="60" height="40" x="1410" y="1145" fill="#c8daa4" rx="2" ry="2"/>
    <rect id="rect4223" width="20" height="10" x="1410" y="1187.5" fill="#c8daa4" rx="1" ry="1"/>
    <rect id="rect4251" width="60" height="40" x="1130" y="1095" fill="#c8daa4" rx="2" ry="2"/>
    <rect id="rect5200" width="60" height="40" x="1020" y="1225" fill="#c8daa4" rx="2" ry="2"/>
    <rect id="rect12920" width="60" height="35" x="1020" y="1435" fill="#c8daa4" rx="2" ry="2"/>
    <rect id="rect12942" width="60" height="35" x="1130" y="805" fill="#c8daa4" rx="2" ry="2"/>
    <rect id="rect12964" width="60" height="45" x="1130" y="895" fill="#c8daa4" rx="2" ry="2"/>
    <rect id="rect12990" width="60" height="30" x="1020" y="1020" fill="#c8daa4" rx="2" ry="2"/>
    <rect id="rect13014" width="60" height="35" x="1130" y="735" fill="#c8daa4" rx="2" ry="2"/>
    <rect id="rect5552" width="60" height="35" x="1410" y="945" fill="#c8daa4" rx="2" ry="2"/>
    <rect id="rect5510" width="25" height="10" x="1130" y="842.5" fill="#adc57d" rx="1" ry="1"/>
    <rect id="rect5518" width="30" height="10" x="1020" y="1052.5" fill="#adc57d" rx="1" ry="1"/>
    <rect id="rect5526" width="30" height="10" x="1020" y="1267.5" fill="#adc57d" rx="1" ry="1"/>
    <rect id="rect4807" width="60" height="45" x="1570" y="1285" fill="#c8daa4" rx="2" ry="2"/>
    <a id="a6002" transform="matrix(1.99983 0 0 1.60004 -1189.757 -193.033)" xlink:href="http://dl.acm.org/citation.cfm?id=1792766" xlink:title="Z3: an efficient SMT solver">
      <rect id="rect6004" width="30" height="25" x="1425" y="805" fill="#c8daa4" rx="1.2" ry="1.25"/>
    </a>
    <rect id="rect6066" width="70" height="40" x="1740" y="1095" fill="none" stroke="#000" stroke-width=".5" opacity=".5" rx="2" ry="2"/>
    <a id="a6070" transform="matrix(1.99998 0 0 1.60004 -1189.964 46.967)" xlink:href="http://dl.acm.org/citation.cfm?id=1792766" xlink:title="Z3: an efficient SMT solver">
      <rect id="rect6072" width="30" height="25" x="1425" y="805" fill="#c8daa4" rx="1.2" ry="1.25"/>
    </a>
    <a id="a6095" transform="matrix(1.99976 0 0 1.80011 -1189.648 -54.095)" xlink:href="http://dl.acm.org/citation.cfm?id=1792766" xlink:title="Z3: an efficient SMT solver">
      <rect id="rect6097" width="30" height="25" x="1425" y="805" fill="#c8daa4" rx="1.201" ry="1.111"/>
    </a>
    <rect id="rect5712" width="60" height="45" x="1440" y="785" fill="none" stroke="#adc57d" stroke-width="1" rx="2" ry="2"/>
    <rect id="rect5762" width="60" height="45" x="1050" y="735" fill="#adc57d" rx="2" ry="2"/>
    <rect id="rect5801" width="59.75" height="29.75" x="1810" y="835" fill="none" stroke="#adc57d" stroke-width="1" rx="2" ry="2"/>
    <rect id="rect13497" width="60" height="25" x="1510" y="785" fill="#adc57d" rx="2" ry="2"/>
    <rect id="rect13536" width="60" height="40" x="1220" y="745" fill="#adc57d" rx="2" ry="2"/>
    <rect id="rect13581" width="60" height="25" x="1740" y="800" fill="#adc57d" rx="2" ry="2"/>
    <rect id="rect13585" width="60" height="29.5" x="1130" y="645" fill="none" stroke="#adc57d" stroke-width="1" rx="2" ry="2"/>
    <rect id="rect13635" width="60" height="30" x="1220" y="645" fill="none" stroke="#adc57d" stroke-width="1" rx="2" ry="2"/>
    <rect id="rect15869" width="60" height="50" x="980" y="705" fill="#adc57d" rx="2" ry="2"/>
    <rect id="rect15916" width="59.5" height="45" x="1290" y="745" fill="none" stroke="#adc57d" stroke-width="1" rx="2" ry="2"/>
    <rect id="rect16475" width="60" height="39.5" x="1360" y="755" fill="none" stroke="#adc57d" stroke-width="1" rx="2" ry="2"/>
    <rect id="rect3528" width="60" height="45" x="1600" y="705" fill="#e0dad5" stroke-dasharray="2.8,2.8" rx="2" ry="2"/>
    <rect id="rect13778" width="60" height="40" x="1020" y="945" fill="#e0dad5" rx="2" ry="2"/>
    <rect id="rect13810" width="60" height="40" x="1020" y="1145" fill="#e0dad5" rx="2" ry="2"/>
    <rect id="rect3553" width="60" height="30" x="1210" y="1485" fill="#c8daa4" rx="2" ry="2"/>
    <rect id="rect3566" width="60" height="35" x="1810" y="1335" fill="#c8daa4" rx="2" ry="2"/>
    <rect id="rect3584" width="60" height="35" x="1310" y="1335" fill="#c8daa4" rx="2" ry="2"/>
    <rect id="rect3607" width="25" height="10" x="1310" y="1385" fill="#c8daa4" rx="1" ry="1"/>
    <rect id="rect3613" width="25" height="10" x="1310" y="1372.5" fill="#c8daa4" rx="1" ry="1"/>
    <rect id="rect3619" width="60" height="35" x="1310" y="1435" fill="#c8daa4" rx="2" ry="2"/>
    <rect id="rect3621" width="25" height="10" x="1310" y="1485" fill="#c8daa4" rx="1" ry="1"/>
    <rect id="rect3623" width="25" height="10" x="1310" y="1472.5" fill="#c8daa4" rx="1" ry="1"/>
    <a id="a3617" transform="matrix(1.99976 0 0 2.00026 -1349.648 -215.214)" xlink:href="http://dl.acm.org/citation.cfm?id=1792766" xlink:title="Z3: an efficient SMT solver">
      <rect id="rect3620" width="30" height="25" x="1425" y="805" fill="#c8daa4" rx="1.201" ry="1"/>
    </a>
    <a id="a3663" transform="matrix(1.99976 0 0 2.20026 -1539.648 -676.214)" xlink:href="http://dl.acm.org/citation.cfm?id=1792766" xlink:title="Z3: an efficient SMT solver">
      <rect id="rect3665" width="30" height="25" x="1425" y="805" fill="#c8daa4" rx="1.201" ry=".909"/>
    </a>
  </g>
  <g id="g366" stroke-width=".7" transform="translate(0 -185)" inkscape:groupmode="layer" inkscape:label="language">
    <rect id="rect5066" width="35" height="10" x="585" y="697.5" fill="#f1e05a" rx="1" ry="1"/>
    <rect id="rect4815" width="30" height="10" x="655" y="837.5" fill="#22228f" rx="1" ry="1"/>
  </g>
  <g id="g420" fill="#565248" color="#000" font-family="Roboto" font-size="10" font-weight="300" text-anchor="middle" transform="translate(0 -185)" word-spacing="0" inkscape:groupmode="layer" inkscape:label="group_text">
    <text id="text430" x="245" y="285" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan432" x="245" y="285" sodipodi:role="line">Stanford</tspan>
    </text>
    <text id="text438" x="570" y="620" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" text-anchor="start" sodipodi:linespacing="100%">
      <tspan id="tspan442" x="570" y="620" sodipodi:role="line">Microsoft</tspan> <tspan id="tspan6000" x="570" y="630" sodipodi:role="line">Research</tspan>
    </text>
    <text id="text484" x="650" y="680" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan486" x="650" y="680" sodipodi:role="line">Carnegie Mellon</tspan>
    </text>
    <text id="text518" x="890" y="350" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan520" x="890" y="350" sodipodi:role="line">Chalmers</tspan>
    </text>
    <text id="text530" x="855" y="945" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan532" x="855" y="945" sodipodi:role="line">Portland</tspan>
    </text>
    <text id="text4143" x="245" y="825" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan4149" x="245" y="825" sodipodi:role="line">Purdue</tspan>
    </text>
    <text id="text4156" x="325" y="835" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan4158" x="325" y="835" sodipodi:role="line">Waterloo</tspan>
    </text>
    <text id="text4989" x="245" y="1045" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan4991" x="245" y="1045" sodipodi:role="line">Google</tspan>
    </text>
    <text id="text4993" x="324.5" y="1025" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan4995" x="325" y="1025" letter-spacing="1" style="text-align:center" sodipodi:role="line">IBM</tspan>
    </text>
    <text id="text4267" x="245" y="635" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan4269" x="245.5" y="635" letter-spacing="1" sodipodi:role="line">MIT</tspan>
    </text>
    <text id="text4271" x="245" y="655" letter-spacing="1" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan4273" x="245" y="655" letter-spacing="0" sodipodi:role="line">Washington</tspan>
    </text>
    <text id="text4275" x="245" y="645" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan4277" x="245" y="645" sodipodi:role="line">Virginia</tspan>
    </text>
    <text id="text5216" x="175" y="445" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan5218" x="175" y="445" sodipodi:role="line">New York</tspan>
    </text>
    <text id="text5323" x="855" y="785" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan5327" x="855" y="785" sodipodi:role="line">Stellenbosch</tspan>
    </text>
    <text id="text5331" x="855" y="795" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan5333" x="855" y="795" sodipodi:role="line">Nebraska</tspan>
    </text>
    <text id="text5566" x="525" y="505" letter-spacing="1" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan5568" x="525.5" y="505" style="text-align:center;-inkscape-font-specification:Roboto Light" sodipodi:role="line">SRI</tspan>
    </text>
    <text id="text6034" x="775" y="645" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan6036" x="775" y="645" sodipodi:role="line">Linz</tspan>
    </text>
    <text id="text5746" x="590" y="335" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan5748" x="590" y="335" sodipodi:role="line">Princeton</tspan>
    </text>
    <text id="text5750" x="590" y="325" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan5752" x="590.5" y="325" letter-spacing="1" sodipodi:role="line">MIT</tspan>
    </text>
    <text id="text5754" x="590" y="315" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan5756" x="590" y="315" sodipodi:role="line">Berkeley</tspan>
    </text>
    <text id="text5793" x="165" y="295" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan5795" x="165" y="295" sodipodi:role="line">Michigan</tspan>
    </text>
    <text id="text5797" x="165" y="285" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan5799" x="165" y="285" sodipodi:role="line">Cadence</tspan>
    </text>
    <text id="text13538" x="335" y="305" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan13540" x="335" y="305" sodipodi:role="line">Iowa</tspan>
    </text>
    <text id="text15871" x="95" y="265" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan15873" x="95" y="265" sodipodi:role="line">Rochester</tspan>
    </text>
    <text id="text15875" x="95" y="255" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan15877" x="95" y="255" sodipodi:role="line">Cornell</tspan>
    </text>
    <text id="text5220-2" x="125" y="480" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan5222-6" x="125" y="480" sodipodi:role="line">Iowa</tspan>
    </text>
    <text id="text13804" x="135" y="505" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan13806" x="135" y="505" sodipodi:role="line">Nancy</tspan>
    </text>
    <text id="text3584" x="925" y="895" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan3586" x="925" y="895" sodipodi:role="line">Linköping</tspan>
    </text>
    <text id="text3588" x="925" y="885" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan3590" x="925" y="885" sodipodi:role="line">Brno</tspan>
    </text>
    <text id="text3596" x="925" y="875" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan3598" x="925" y="875" sodipodi:role="line">Sinica</tspan>
    </text>
    <text id="text3600" x="925" y="865" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan3602" x="925" y="865" sodipodi:role="line">Uppsala</tspan>
    </text>
    <text id="text3603" x="425" y="885" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan3605" x="425" y="885" sodipodi:role="line">Singapore</tspan>
    </text>
    <text id="text3646" x="615" y="955" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan3648" x="615" y="955" sodipodi:role="line">California, Santa Barbara</tspan>
    </text>
    <text id="text3711" x="425" y="655" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan3713" x="425" y="655" sodipodi:role="line">Virginia</tspan>
    </text>
  </g>
  <g id="g582" font-weight="500" transform="translate(0 -185)" word-spacing="0" inkscape:groupmode="layer" inkscape:label="box_text">
    <text id="text_green" x="830" y="815" fill="#363228" font-family="Roboto" font-size="10" font-weight="300" letter-spacing="0" style="text-align:start;line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan862" x="830" y="815" fill="#516817" sodipodi:role="line">Green</tspan> <tspan id="tspan864" x="830" y="825" fill="#516817" sodipodi:role="line">solver</tspan> <tspan id="tspan5335" x="830" y="831.833" font-size="6" sodipodi:role="line">2012</tspan> <tspan id="tspan5337" x="830" y="837.833" font-size="6" sodipodi:role="line">persistent cache</tspan>
    </text>
    <text id="text972" x="220" y="575" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan974" x="220" y="575" font-size="10" letter-spacing="1" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">STP</tspan> <tspan id="tspan976" x="220" y="581.833" sodipodi:role="line">2007</tspan>
    </text>
    <a id="text_z3" transform="translate(-15 240)" xlink:href="http://dl.acm.org/citation.cfm?id=1792766" xlink:title="Z3: an efficient SMT solver">
      <text id="text1258" x="1430" y="832.362" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" transform="translate(-915 -447.362)" sodipodi:linespacing="100%">
        <tspan id="tspan1260" x="1430" y="832.362" font-size="10" letter-spacing="1" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">Z3</tspan> <tspan id="tspan5187" x="1430" y="839.195" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">2008</tspan> <tspan id="tspan5189" x="1430" y="845.195" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line"><tspan id="tspan5495" letter-spacing=".5">SMT</tspan> solver,</tspan> <tspan id="tspan5497" x="1430" y="851.195" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">SAT: DPLL</tspan>
      </text>
    </a>
    <text id="text1266" x="830" y="415" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan1268" x="830" y="415" font-size="10" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">Mini<tspan id="tspan1270" letter-spacing="1" style="-inkscape-font-specification:Roboto Light">SAT</tspan> </tspan> <tspan id="tspan1272" x="830" y="421.833" sodipodi:role="line">2003</tspan> <tspan id="tspan5710" x="830" y="427.833" sodipodi:role="line">extensible,</tspan> <tspan id="tspan15914" x="830" y="433.833" sodipodi:role="line">CDCL-based</tspan>
    </text>
    <text id="text1284" x="229.75" y="599.5" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" text-anchor="middle" sodipodi:linespacing="100%">
      <tspan id="tspan1286" x="230" y="599.5" style="text-align:center;line-height:50%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">Mini<tspan id="tspan1288" letter-spacing=".5" style="text-align:center;-inkscape-font-specification:Roboto Light">SAT</tspan> </tspan>
    </text>
    <text id="text1310" x="830" y="965" fill="#363228" font-family="Roboto" font-size="10" font-weight="300" letter-spacing="0" style="text-align:start;line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan1312" x="830" y="965" letter-spacing="1" style="-inkscape-font-specification:Roboto Light" sodipodi:role="line">BLT</tspan> <tspan id="tspan5511" x="830" y="971.833" font-size="6" style="-inkscape-font-specification:Roboto Light" sodipodi:role="line">bounded integer</tspan> <tspan id="tspan5513" x="830" y="977.833" font-size="6" style="-inkscape-font-specification:Roboto Light" sodipodi:role="line">linear constraints</tspan>
    </text>
    <text id="text1354" x="500" y="865" fill="#363228" font-family="Roboto" font-size="10" font-weight="300" letter-spacing="0" style="text-align:start;line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan1356" x="500" y="865" sodipodi:role="line">Lean</tspan> <tspan id="tspan1358" x="500" y="871.833" font-size="6" style="-inkscape-font-specification:Roboto Light" sodipodi:role="line">2013</tspan>
    </text>
    <text id="text1474" x="545.056" y="237.168" fill="#565248" color="#000" font-family="Roboto" font-size="24" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" text-anchor="middle" sodipodi:linespacing="100%">
      <tspan id="tspan1476" x="545.056" y="237.168" sodipodi:role="line">Solving Timeline</tspan>
    </text>
    <text id="text4113" x="590" y="865" fill="#363228" font-family="Roboto" font-size="10" font-weight="300" letter-spacing="0" style="text-align:start;line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan4116" x="590" y="865" sodipodi:role="line">dReal</tspan> <tspan id="tspan4118" x="590" y="871.833" font-size="6" style="-inkscape-font-specification:Roboto Light" sodipodi:role="line">2013</tspan>
    </text>
    <text id="text4129" x="220" y="865" fill="#363228" font-family="Roboto" font-size="10" font-weight="300" letter-spacing="0" style="text-align:start;line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan4131" x="220" y="865" sodipodi:role="line">Z3-str</tspan> <tspan id="tspan4133" x="220" y="871.833" font-size="6" style="-inkscape-font-specification:Roboto Light" sodipodi:role="line">2013</tspan>
    </text>
    <text id="text4193" x="224.75" y="889.5" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" text-anchor="middle" sodipodi:linespacing="100%">
      <tspan id="tspan4195" x="225" y="889.5" letter-spacing=".5" style="text-align:center;line-height:50%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">Z3</tspan>
    </text>
    <text id="text4969" x="220" y="1065" fill="#363228" font-family="Roboto" font-size="10" font-weight="300" letter-spacing="0" style="text-align:start;line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan4971" x="220" y="1065" sodipodi:role="line">Z3str2</tspan> <tspan id="tspan4973" x="220" y="1071.833" font-size="6" style="-inkscape-font-specification:Roboto Light" sodipodi:role="line">2017</tspan>
    </text>
    <text id="text4977" x="224.75" y="1089.5" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" text-anchor="middle" sodipodi:linespacing="100%">
      <tspan id="tspan4979" x="225" y="1089.5" letter-spacing=".5" style="text-align:center;line-height:50%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">Z3</tspan>
    </text>
    <text id="text5027" x="590" y="725" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan5031" x="590" y="725" font-size="10" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">Kudzu</tspan> <tspan id="tspan5033" x="590" y="731.833" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">2010</tspan> <tspan id="tspan5072" x="590" y="737.833" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">symbolic</tspan> <tspan id="tspan5074" x="590" y="743.833" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">execution</tspan>
    </text>
    <text id="text5084" x="632.5" y="725" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan5086" x="632.5" y="725" font-size="10" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">Kaluza</tspan> <tspan id="tspan5088" x="632.5" y="731.833" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">2010</tspan> <tspan id="tspan5092" x="632.5" y="737.833" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">SMT, regex,</tspan> <tspan id="tspan5096" x="632.5" y="743.833" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">strings</tspan>
    </text>
    <text id="text4225" x="500" y="725" fill="#363228" font-family="Roboto" font-size="10" font-weight="300" letter-spacing="0" style="text-align:start;line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan4227" x="500" y="725" sodipodi:role="line">Rex</tspan> <tspan id="tspan4229" x="500" y="731.833" font-size="6" style="-inkscape-font-specification:Roboto Light" sodipodi:role="line">2010</tspan> <tspan id="tspan4247" x="500" y="737.833" font-size="6" style="-inkscape-font-specification:Roboto Light" sodipodi:role="line">regular</tspan> <tspan id="tspan4249" x="500" y="743.833" font-size="6" style="-inkscape-font-specification:Roboto Light" sodipodi:role="line">expressions</tspan>
    </text>
    <text id="text4231" x="504.75" y="759.5" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" text-anchor="middle" sodipodi:linespacing="100%">
      <tspan id="tspan4233" x="505" y="759.5" letter-spacing=".5" style="text-align:center;line-height:50%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">Z3</tspan>
    </text>
    <text id="text4253" x="220" y="675" fill="#363228" font-family="Roboto" font-size="10" font-weight="300" letter-spacing="0" style="text-align:start;line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan4255" x="220" y="675" letter-spacing="1" sodipodi:role="line">HAMPI</tspan> <tspan id="tspan4257" x="220" y="681.833" font-size="6" style="-inkscape-font-specification:Roboto Light" sodipodi:role="line">2009</tspan> <tspan id="tspan4261" x="220" y="687.833" font-size="6" style="-inkscape-font-specification:Roboto Light" sodipodi:role="line">string</tspan> <tspan id="tspan4265" x="220" y="693.833" font-size="6" style="-inkscape-font-specification:Roboto Light" sodipodi:role="line">constraints</tspan>
    </text>
    <text id="text5202" x="110" y="805" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan5206" x="110" y="805" font-size="10" letter-spacing="1" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">CVC4</tspan> <tspan id="tspan5208" x="110" y="811.833" sodipodi:role="line">2011</tspan> <tspan id="tspan12938" x="110" y="817.833" sodipodi:role="line">DPLL(T)</tspan> <tspan id="tspan12940" x="110" y="823.833" sodipodi:role="line">SMT solver</tspan>
    </text>
    <text id="text12922" x="110" y="1010" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan12924" x="110" y="1010" letter-spacing=".5" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">CVC4</tspan> <tspan id="tspan12926" x="110" y="1016" sodipodi:role="line">2016</tspan> <tspan id="tspan12928" x="110" y="1022" sodipodi:role="line">with string</tspan> <tspan id="tspan12930" x="110" y="1028" sodipodi:role="line">constraints</tspan>
    </text>
    <text id="text12944" x="220" y="385" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan12946" x="220" y="385" font-size="10" letter-spacing="1" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">CVC</tspan> <tspan id="tspan12948" x="220" y="391.833" sodipodi:role="line">2002</tspan> <tspan id="tspan12952" x="220" y="397.833" sodipodi:role="line">SMT solver</tspan>
    </text>
    <text id="text12966" x="220" y="475" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan12968" x="220" y="475" font-size="10" letter-spacing="1" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">CVC</tspan> <tspan id="tspan12986" x="220" y="485" font-size="10" letter-spacing="1" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line"> <tspan id="tspan12988" letter-spacing="0">Lite</tspan> </tspan> <tspan id="tspan12970" x="220" y="491.833" sodipodi:role="line">2004</tspan> <tspan id="tspan12972" x="220" y="497.833" sodipodi:role="line">SMT solver</tspan>
    </text>
    <text id="text12992" x="110" y="600" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan12994" x="110" y="600" font-size="10" letter-spacing="1" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">CVC3</tspan> <tspan id="tspan13000" x="110" y="606.833" sodipodi:role="line">2007</tspan>
    </text>
    <text id="text13016" x="220" y="315" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan13018" x="220" y="315" font-size="10" letter-spacing="1" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">SVC</tspan> <tspan id="tspan13020" x="220" y="321.833" sodipodi:role="line">1996</tspan> <tspan id="tspan13022" x="220" y="327.833" sodipodi:role="line">validity checker</tspan>
    </text>
    <text id="text5554" x="500" y="525" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan5558" x="500" y="525" font-size="10" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">Yices</tspan> <tspan id="tspan5560" x="500" y="531.833" sodipodi:role="line">2006</tspan> <tspan id="tspan5572" x="500" y="537.833" sodipodi:role="line"><tspan id="tspan5580" letter-spacing=".5">SMT</tspan> solver</tspan>
    </text>
    <text id="text5512" x="227.25" y="414.5" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" text-anchor="middle" sodipodi:linespacing="100%">
      <tspan id="tspan5514" x="227.25" y="414.5" style="text-align:center;line-height:50%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">Chaff</tspan>
    </text>
    <text id="text5520" x="119.75" y="624.5" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" text-anchor="middle" sodipodi:linespacing="100%">
      <tspan id="tspan5522" x="120" y="624.5" style="text-align:center;line-height:50%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">Mini<tspan id="tspan5524" letter-spacing=".5" style="text-align:center;-inkscape-font-specification:Roboto Light">SAT</tspan> </tspan>
    </text>
    <text id="text5528" x="119.75" y="839.5" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" text-anchor="middle" sodipodi:linespacing="100%">
      <tspan id="tspan5530" x="120" y="839.5" style="text-align:center;line-height:50%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">Mini<tspan id="tspan5532" letter-spacing=".5" style="text-align:center;-inkscape-font-specification:Roboto Light">SAT</tspan> </tspan>
    </text>
    <text id="text4809" x="660" y="865" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan4811" x="660" y="865" font-size="10" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">Rosette</tspan> <tspan id="tspan4813" x="660" y="871.833" sodipodi:role="line">2013</tspan> <tspan id="tspan5593" x="660" y="877.833" sodipodi:role="line">symbolic</tspan> <tspan id="tspan5589" x="660" y="883.833" sodipodi:role="line">virtual</tspan> <tspan id="tspan5591" x="660" y="889.833" sodipodi:role="line">machine</tspan>
    </text>
    <a id="a6006" transform="translate(235 290)" xlink:href="http://dl.acm.org/citation.cfm?id=1792766" xlink:title="Z3: an efficient SMT solver">
      <text id="text6008" x="1430" y="832.362" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" transform="translate(-915 -447.362)" sodipodi:linespacing="100%">
        <tspan id="tspan6010" x="1430" y="832.362" font-size="10" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">Boolector</tspan> <tspan id="tspan6012" x="1430" y="839.195" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">2009</tspan> <tspan id="tspan6018" x="1430" y="845.195" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line"><tspan id="tspan6016" letter-spacing=".5">SMT</tspan> solver</tspan>
      </text>
    </a>
    <a id="a6038" transform="translate(315 290)" xlink:href="http://dl.acm.org/citation.cfm?id=1792766" xlink:title="Z3: an efficient SMT solver">
      <text id="text6040" x="1430" y="832.362" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" transform="translate(-915 -447.362)" sodipodi:linespacing="100%">
        <tspan id="tspan6042" x="1430" y="832.362" font-size="7.5" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">Minimizing</tspan> <tspan id="tspan6064" x="1430" y="839.862" font-size="7.5" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">Learned Clauses</tspan> <tspan id="tspan6046" x="1430" y="846.174" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">2009</tspan>
      </text>
    </a>
    <a id="a6074" transform="translate(235 530)" xlink:href="http://dl.acm.org/citation.cfm?id=1792766" xlink:title="Z3: an efficient SMT solver">
      <text id="text6076" x="1430" y="832.362" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" transform="translate(-915 -447.362)" sodipodi:linespacing="100%">
        <tspan id="tspan6078" x="1430" y="832.362" font-size="10" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">PBoolector</tspan> <tspan id="tspan6080" x="1430" y="839.195" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">2014</tspan> <tspan id="tspan6082" x="1430" y="845.195" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">parallel sovler</tspan>
      </text>
    </a>
    <a id="a6099" transform="translate(235 590)" xlink:href="http://dl.acm.org/citation.cfm?id=1792766" xlink:title="Z3: an efficient SMT solver">
      <text id="text6101" x="1430" y="832.362" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" transform="translate(-915 -447.362)" sodipodi:linespacing="100%">
        <tspan id="tspan6103" x="1430" y="832.362" font-size="10" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">Boolector</tspan> <tspan id="tspan3554" x="1430" y="842.362" font-size="10" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">2.0</tspan> <tspan id="tspan6105" x="1430" y="849.195" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">2015</tspan> <tspan id="tspan6107" x="1430" y="855.195" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line"><tspan id="tspan6109" letter-spacing=".5">SMT</tspan> solver</tspan>
      </text>
    </a>
    <text id="text5696" x="854.5" y="376.5" fill="#363228" color="#000" font-family="Roboto" font-size="8" font-weight="300" letter-spacing=".5" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" text-anchor="middle" sodipodi:linespacing="100%">
      <tspan id="tspan5702" x="854.75" y="376.5" style="text-align:center;line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">SATZOO</tspan> <tspan id="tspan16513" x="854.75" y="384.5" style="text-align:center;line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">SATNIK</tspan>
    </text>
    <text id="text5714" x="530" y="365" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan5716" x="530" y="365" font-size="10" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">Chaff</tspan> <tspan id="tspan5722" x="530" y="371.833" sodipodi:role="line">2001</tspan> <tspan id="tspan5758" x="530" y="377.833" sodipodi:role="line">dynamic variable</tspan> <tspan id="tspan5760" x="530" y="383.833" sodipodi:role="line">ordering, watched</tspan> <tspan id="tspan6340" x="530" y="389.833" sodipodi:role="line">literals</tspan>
    </text>
    <text id="text5764" x="140" y="315" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan5766" x="140" y="315" font-size="10" letter-spacing="1" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">GRASP</tspan> <tspan id="tspan5768" x="140" y="321.833" sodipodi:role="line">1996</tspan> <tspan id="tspan5772" x="140" y="327.833" sodipodi:role="line">conflict-driven</tspan> <tspan id="tspan5776" x="140" y="333.833" sodipodi:role="line">backtracking,</tspan> <tspan id="tspan13528" x="140" y="339.833" sodipodi:role="line">clause learning</tspan>
    </text>
    <text id="text5803" x="900" y="410" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan5809" x="900" y="410" font-size="8" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">Incremental</tspan> <tspan id="tspan6334" x="900" y="418" font-size="8" letter-spacing=".5" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">SAT</tspan> <tspan id="tspan5811" x="900" y="424.417" sodipodi:role="line">2003</tspan>
    </text>
    <text id="text13499" x="625" y="361.5" fill="#363228" color="#000" font-family="Roboto" font-size="8" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" text-anchor="middle" sodipodi:linespacing="100%">
      <tspan id="tspan16507" x="625" y="361.5" style="text-align:center;line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">zChaff</tspan> <tspan id="tspan16511" x="625" y="369.5" style="text-align:center;line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">mChaff</tspan>
    </text>
    <text id="text13546" x="310" y="325" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan13548" x="310" y="325" font-size="10" letter-spacing="1" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">SATO</tspan> <tspan id="tspan13550" x="310" y="331.833" sodipodi:role="line">1997</tspan> <tspan id="tspan13556" x="310" y="337.833" sodipodi:role="line">propositional</tspan> <tspan id="tspan13571" x="310" y="343.833" sodipodi:role="line">prover, <tspan id="tspan13573" letter-spacing=".5">DP</tspan> </tspan>
    </text>
    <text id="text13587" x="220" y="225" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan13589" x="220" y="225" font-size="10" letter-spacing="1" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">DP</tspan> <tspan id="tspan13597" x="220" y="231.833" sodipodi:role="line">1960</tspan>
    </text>
    <text id="text13645" x="310" y="225" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan13647" x="310" y="225" font-size="10" letter-spacing="1" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">DPLL</tspan> <tspan id="tspan13649" x="310" y="231.833" sodipodi:role="line">1962</tspan>
    </text>
    <text id="text15859" x="690" y="285" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan15861" x="690" y="285" font-size="10" letter-spacing="1" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">DIMACS-</tspan> <tspan id="tspan8154" x="690" y="295" font-size="10" letter-spacing="1" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">CNF</tspan> <tspan id="tspan15863" x="690" y="301.833" sodipodi:role="line">1993</tspan> <tspan id="tspan15865" x="690" y="307.833" sodipodi:role="line"><tspan id="tspan15867" letter-spacing=".5">CNF</tspan> input format</tspan>
    </text>
    <text id="text15879" x="70" y="285" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan15881" x="70" y="285" font-size="10" letter-spacing="1" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">GSAT</tspan> <tspan id="tspan15910" x="70" y="295" font-size="10" letter-spacing="1" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">WSAT</tspan> <tspan id="tspan15883" x="70" y="301.833" sodipodi:role="line">1993</tspan> <tspan id="tspan15889" x="70" y="307.833" sodipodi:role="line">stochastic</tspan> <tspan id="tspan15902" x="70" y="313.833" sodipodi:role="line">local search</tspan>
    </text>
    <text id="text15926" x="380" y="325" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan15928" x="380" y="325" font-size="10" letter-spacing="1" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">PPZ</tspan> <tspan id="tspan15930" x="380" y="331.833" sodipodi:role="line">1997</tspan> <tspan id="tspan16469" x="380" y="337.833" sodipodi:role="line">for <tspan id="tspan16471" font-style="italic" style="-inkscape-font-specification:Roboto Light Italic">k</tspan> -<tspan id="tspan16473" letter-spacing=".5">CNF</tspan> </tspan> <tspan id="tspan15936" x="380" y="343.833" sodipodi:role="line">satisfiability</tspan> <tspan id="tspan15951" x="380" y="349.833" sodipodi:role="line">coding lemma</tspan>
    </text>
    <text id="text16477" x="450" y="335" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan16479" x="450" y="335" font-size="10" letter-spacing="1" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">PPSZ</tspan> <tspan id="tspan16481" x="450" y="341.833" sodipodi:role="line">1998</tspan> <tspan id="tspan16483" x="450" y="347.833" sodipodi:role="line">for <tspan id="tspan16485" font-style="italic" style="-inkscape-font-specification:Roboto Light Italic">k</tspan> -<tspan id="tspan16487" letter-spacing=".5">CNF</tspan> </tspan> <tspan id="tspan16491" x="450" y="353.833" sodipodi:role="line">improved <tspan id="tspan16505" letter-spacing=".5">PPZ</tspan> </tspan>
    </text>
    <text id="text13780" x="110" y="525" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan13788" x="110" y="525" font-size="10" letter-spacing="1" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">SMT-LIB</tspan> <tspan id="tspan13784" x="110" y="531.833" sodipodi:role="line">2006</tspan> <tspan id="tspan8162" x="110" y="537.833" sodipodi:role="line">SMT formula</tspan> <tspan id="tspan8164" x="110" y="543.833" sodipodi:role="line">format</tspan>
    </text>
    <text id="text13812" x="110" y="725" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan13814" x="110" y="725" font-size="10" letter-spacing="1" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">SMT-</tspan> <tspan id="tspan13816" x="110" y="735" font-size="10" letter-spacing="1" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">LIB <tspan id="tspan13818" letter-spacing="0">2</tspan> </tspan> <tspan id="tspan13820" x="110" y="741.833" sodipodi:role="line">2006</tspan>
    </text>
    <text id="text3555" x="300" y="1065" fill="#363228" font-family="Roboto" font-size="10" font-weight="300" letter-spacing="0" style="text-align:start;line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan3557" x="300" y="1065" sodipodi:role="line">Z3str3</tspan> <tspan id="tspan3559" x="300" y="1071.833" font-size="6" style="-inkscape-font-specification:Roboto Light" sodipodi:role="line">2017</tspan>
    </text>
    <text id="text3568" x="900" y="915" fill="#363228" font-family="Roboto" font-size="10" font-weight="300" letter-spacing="0" style="text-align:start;line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan3570" x="900" y="915" sodipodi:role="line">Norn</tspan> <tspan id="tspan3572" x="900" y="921.833" font-size="6" style="-inkscape-font-specification:Roboto Light" sodipodi:role="line">2014</tspan> <tspan id="tspan3580" x="900" y="927.833" font-size="6" style="-inkscape-font-specification:Roboto Light" sodipodi:role="line">string constraints</tspan>
    </text>
    <text id="text3586" x="400" y="915" fill="#363228" font-family="Roboto" font-size="10" font-weight="300" letter-spacing="0" style="text-align:start;line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan3588" x="400" y="915" letter-spacing="1" sodipodi:role="line">S3</tspan> <tspan id="tspan3591" x="400" y="921.833" font-size="6" style="-inkscape-font-specification:Roboto Light" sodipodi:role="line">2014</tspan> <tspan id="tspan3597" x="400" y="927.833" font-size="6" style="-inkscape-font-specification:Roboto Light" sodipodi:role="line">string solver</tspan>
    </text>
    <text id="text3609" x="407.25" y="957" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" text-anchor="middle" sodipodi:linespacing="100%">
      <tspan id="tspan3611" x="407.25" y="957" style="text-align:center;line-height:50%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">Z3-str</tspan>
    </text>
    <text id="text3615" x="407.25" y="944.5" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" text-anchor="middle" sodipodi:linespacing="100%">
      <tspan id="tspan3617" x="407.5" y="944.5" letter-spacing=".5" style="text-align:center;line-height:50%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">Z3</tspan>
    </text>
    <text id="text3629" x="400" y="1015" fill="#363228" font-family="Roboto" font-size="10" font-weight="300" letter-spacing="0" style="text-align:start;line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan3631" x="400" y="1015" letter-spacing="1" sodipodi:role="line">S3P</tspan> <tspan id="tspan3633" x="400" y="1021.833" font-size="6" style="-inkscape-font-specification:Roboto Light" sodipodi:role="line">2016</tspan> <tspan id="tspan3635" x="400" y="1027.833" font-size="6" style="-inkscape-font-specification:Roboto Light" sodipodi:role="line">progressive S3</tspan>
    </text>
    <text id="text3637" x="407.25" y="1057" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" text-anchor="middle" sodipodi:linespacing="100%">
      <tspan id="tspan3639" x="407.25" y="1057" style="text-align:center;line-height:50%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">Z3-str</tspan>
    </text>
    <text id="text3641" x="407.25" y="1044.5" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" text-anchor="middle" sodipodi:linespacing="100%">
      <tspan id="tspan3643" x="407.5" y="1044.5" letter-spacing=".5" style="text-align:center;line-height:50%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">Z3</tspan>
    </text>
    <a id="a3622" transform="translate(75 590)" xlink:href="http://dl.acm.org/citation.cfm?id=1792766" xlink:title="Z3: an efficient SMT solver">
      <text id="text3624" x="1430" y="832.362" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" transform="translate(-915 -447.362)" sodipodi:linespacing="100%">
        <tspan id="tspan3628" x="1430" y="832.362" font-size="10" letter-spacing="1" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">ABC</tspan> <tspan id="tspan3630" x="1430" y="839.195" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">2015</tspan> <tspan id="tspan3632" x="1430" y="845.195" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">automata-based</tspan> <tspan id="tspan3650" x="1430" y="851.195" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">model counting for</tspan> <tspan id="tspan3652" x="1430" y="857.195" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">string constraints</tspan>
      </text>
    </a>
    <a id="a3667" transform="translate(-15 590)" xlink:href="http://dl.acm.org/citation.cfm?id=1792766" xlink:title="Z3: an efficient SMT solver">
      <text id="text3669" x="415" y="85" fill="#363228" color="#000" font-family="Roboto" font-size="6" font-weight="300" letter-spacing="0" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
        <tspan id="tspan3671" x="415" y="85" font-size="10" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">DPrle</tspan> <tspan id="tspan3673" x="415" y="91.833" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">2015</tspan> <tspan id="tspan3679" x="415" y="97.833" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">decision procedure</tspan> <tspan id="tspan3696" x="415" y="103.833" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">for subset</tspan> <tspan id="tspan3707" x="415" y="109.833" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">constraints over</tspan> <tspan id="tspan3709" x="415" y="115.833" style="line-height:100%;-inkscape-font-specification:Roboto Light" sodipodi:role="line">regular languages</tspan>
      </text>
    </a>
  </g>
  <g id="g1514" color="#000" font-family="Roboto" font-size="6" font-weight="700" letter-spacing="0" text-anchor="middle" transform="translate(0 -185)" word-spacing="0" inkscape:groupmode="layer" inkscape:label="language_text">
    <text id="text5068" x="602.5" y="704.5" opacity=".85" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Bold" sodipodi:linespacing="100%">
      <tspan id="tspan5070" x="602.5" y="704.5" style="text-align:center;line-height:50%;-inkscape-font-specification:Roboto Bold" sodipodi:role="line">JavaScript</tspan>
    </text>
    <text id="text4817" x="669.75" y="844.5" fill="#fff" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Bold" sodipodi:linespacing="100%">
      <tspan id="tspan4819" x="669.75" y="844.5" style="text-align:center;line-height:50%;-inkscape-font-specification:Roboto Bold" sodipodi:role="line">Rosette</tspan>
    </text>
  </g>
  <g id="g1622" fill="#565248" color="#000" font-family="Roboto" font-size="10" font-weight="300" letter-spacing="0" text-anchor="end" transform="translate(-915 -620)" word-spacing="0" inkscape:groupmode="layer" inkscape:label="time_text">
    <text id="text1624" x="960" y="800" overflow="visible" style="text-indent:0;text-align:end;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan1626" x="960" y="800" sodipodi:role="line">2001</tspan>
    </text>
    <text id="text1628" x="960" y="820" overflow="visible" style="text-indent:0;text-align:end;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan1630" x="960" y="820" sodipodi:role="line">2002</tspan>
    </text>
    <text id="text1632" x="960" y="850" overflow="visible" style="text-indent:0;text-align:end;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan1634" x="960" y="850" sodipodi:role="line">2003</tspan>
    </text>
    <text id="text1636" x="960" y="880" overflow="visible" style="text-indent:0;text-align:end;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan1638" x="960" y="880" sodipodi:role="line">2004</tspan>
    </text>
    <text id="text1640" x="960" y="920" overflow="visible" style="text-indent:0;text-align:end;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan1642" x="960" y="920" sodipodi:role="line">2005</tspan>
    </text>
    <text id="text1644" x="960" y="970" overflow="visible" style="text-indent:0;text-align:end;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan1646" x="960" y="970" sodipodi:role="line">2006</tspan>
    </text>
    <text id="text1648" x="960" y="1020" overflow="visible" style="text-indent:0;text-align:end;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan1650" x="960" y="1020" sodipodi:role="line">2007</tspan>
    </text>
    <text id="text1652" x="960" y="1070" overflow="visible" style="text-indent:0;text-align:end;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan1654" x="960" y="1070" sodipodi:role="line">2008</tspan>
    </text>
    <text id="text1656" x="960" y="1120" overflow="visible" style="text-indent:0;text-align:end;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan1658" x="960" y="1120" sodipodi:role="line">2009</tspan>
    </text>
    <text id="text1660" x="960" y="1170" overflow="visible" style="text-indent:0;text-align:end;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan1662" x="960" y="1170" sodipodi:role="line">2010</tspan>
    </text>
    <text id="text1664" x="960" y="1210" overflow="visible" style="text-indent:0;text-align:end;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan1666" x="960" y="1210" sodipodi:role="line">2011</tspan>
    </text>
    <text id="text1668" x="960" y="1260" overflow="visible" style="text-indent:0;text-align:end;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan1670" x="960" y="1260" sodipodi:role="line">2012</tspan>
    </text>
    <text id="text1672" x="960" y="1310" overflow="visible" style="text-indent:0;text-align:end;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan1674" x="960" y="1310" sodipodi:role="line">2013</tspan>
    </text>
    <text id="text1676" x="960" y="1360" overflow="visible" style="text-indent:0;text-align:end;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan1678" x="960" y="1360" sodipodi:role="line">2014</tspan>
    </text>
    <text id="text1680" x="960" y="1410" overflow="visible" style="text-indent:0;text-align:end;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan1682" x="960" y="1410" sodipodi:role="line">2015</tspan>
    </text>
    <text id="text1684" x="960" y="1460" overflow="visible" style="text-indent:0;text-align:end;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan1686" x="960" y="1460" sodipodi:role="line">2016</tspan>
    </text>
    <text id="text1688" x="960" y="1510" overflow="visible" style="text-indent:0;text-align:end;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan1690" x="960" y="1510" sodipodi:role="line">2017</tspan>
    </text>
    <text id="text1704" x="960" y="740" overflow="visible" style="text-indent:0;text-align:end;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan1706" x="960" y="740" sodipodi:role="line">1996</tspan>
    </text>
    <text id="text1708" x="960" y="760" overflow="visible" style="text-indent:0;text-align:end;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan1710" x="960" y="760" sodipodi:role="line">1998</tspan>
    </text>
    <text id="text1712" x="960" y="780" overflow="visible" style="text-indent:0;text-align:end;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan1714" x="960" y="780" sodipodi:role="line">2000</tspan>
    </text>
    <text id="text3474" x="960" y="720" overflow="visible" style="text-indent:0;text-align:end;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan3476" x="960" y="720" sodipodi:role="line">1994</tspan>
    </text>
    <text id="text3478" x="960" y="700" overflow="visible" style="text-indent:0;text-align:end;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan3480" x="960" y="700" sodipodi:role="line">1992</tspan>
    </text>
    <text id="text3482" x="960" y="680" overflow="visible" style="text-indent:0;text-align:end;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan3484" x="960" y="680" sodipodi:role="line">1990</tspan>
    </text>
    <text id="text3486" x="960" y="660" overflow="visible" style="text-indent:0;text-align:end;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan3488" x="960" y="660" sodipodi:role="line">1970</tspan>
    </text>
  </g>
  <g id="g1756" fill="none" stroke="#363228" stroke-linecap="round" stroke-width=".5" transform="translate(0 -185)" inkscape:groupmode="layer" inkscape:label="arrows">
    <path id="path5582" d="M240 545h-50" inkscape:connector-curvature="0" sodipodi:nodetypes="cc"/>
    <path id="path5584" stroke-linejoin="round" d="M193 547c-1-2-3-2-3-2s2 0 3-2" inkscape:connector-curvature="0" sodipodi:nodetypes="ccc"/>
    <path id="path5590" d="M540 550v55" inkscape:connector-curvature="0" sodipodi:nodetypes="cc"/>
    <path id="path5592" stroke-linejoin="round" d="M542 602c-2 1-2 3-2 3s0-2-2-3" inkscape:connector-curvature="0" sodipodi:nodetypes="ccc"/>
    <path id="path15827" d="M275 725h10c6 0 10 4 10 10v110" inkscape:connector-curvature="0" sodipodi:nodetypes="cccc"/>
    <path id="path15829" stroke-linejoin="round" d="M297 842c-2 1-2 3-2 3s0-2-2-3" inkscape:connector-curvature="0" sodipodi:nodetypes="ccc"/>
    <path id="path3610" d="M275 1020h10c6 0 10 4 10 10v10" inkscape:connector-curvature="0" sodipodi:nodetypes="cccc"/>
    <path id="path3612" stroke-linejoin="round" d="M297 1037c-2 1-2 3-2 3s0-2-2-3" inkscape:connector-curvature="0" sodipodi:nodetypes="ccc"/>
    <path id="path3569" stroke="#adc57d" d="M340 1080v15" inkscape:connector-curvature="0" sodipodi:nodetypes="cc"/>
    <path id="path3571" stroke="#adc57d" stroke-linejoin="round" d="M338 1092c2 1 2 3 2 3s0-2 2-3" inkscape:connector-curvature="0" sodipodi:nodetypes="ccc"/>
  </g>
  <g id="g1762" fill="#363228" color="#000" font-family="Roboto" font-weight="300" letter-spacing="0" transform="translate(0 -185)" word-spacing="0" inkscape:groupmode="layer" inkscape:label="people">
    <text id="text1788" x="215" y="610" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan1790" x="215" y="610" sodipodi:role="line">V. Ganesh</tspan> <tspan id="tspan1794" x="215" y="616" sodipodi:role="line">D. Dill</tspan>
    </text>
    <text id="text1944" x="824.461" y="449.5" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan1946" x="824.461" y="449.5" sodipodi:role="line">N. Eén</tspan> <tspan id="tspan1948" x="824.461" y="455.5" sodipodi:role="line">N. Sörensson</tspan>
    </text>
    <text id="text1970" x="495" y="660" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan1972" x="495" y="660" sodipodi:role="line">L. de Moura</tspan> <tspan id="tspan5193" x="495" y="666" sodipodi:role="line">N. Bjørner</tspan>
    </text>
    <text id="text1974" x="495" y="890" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan1976" x="495" y="890" sodipodi:role="line">L. de Moura</tspan> <tspan id="tspan3567" x="495" y="896" sodipodi:role="line">S. Kong</tspan>
    </text>
    <text id="text2040" x="930" y="236.5" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan2042" x="930" y="236.5" sodipodi:role="line"> <tspan id="tspan4030" letter-spacing=".5">SAT</tspan> <tspan id="tspan15852">solving</tspan> </tspan>
    </text>
    <text id="text4853" x="930" y="221.5" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan4855" x="930" y="221.5" style="line-height:100%" sodipodi:role="line"><tspan id="tspan15857" letter-spacing=".5">SMT</tspan> solving</tspan>
    </text>
    <text id="text4120" x="585" y="890" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan4122" x="585" y="890" sodipodi:role="line">S. Kong</tspan>
    </text>
    <text id="text4135" x="215" y="900" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan4137" x="215" y="900" sodipodi:role="line">Y. Zheng (P)</tspan> <tspan id="tspan4139" x="215" y="906" sodipodi:role="line">X. Zhang (P)</tspan> <tspan id="tspan4141" x="215" y="912" sodipodi:role="line">V. Ganesh (W)</tspan>
    </text>
    <text id="text4164" x="299.909" y="779.941" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan4166" x="299.909" y="779.941" sodipodi:role="line">V. Ganesh</tspan>
    </text>
    <text id="text4981" x="215" y="1100" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan4983" x="215" y="1100" sodipodi:role="line">Y. Zheng (I)</tspan> <tspan id="tspan4985" x="215" y="1106" sodipodi:role="line">X. Zhang (P)</tspan> <tspan id="tspan4987" x="215" y="1112" sodipodi:role="line">V. Ganesh (W)</tspan> <tspan id="tspan4997" x="215" y="1118" sodipodi:role="line">...</tspan>
    </text>
    <text id="text5035" x="585" y="760" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan5043" x="585" y="760" sodipodi:role="line">P. Saxena</tspan> <tspan id="tspan5054" x="585" y="766" sodipodi:role="line">D. Akhawe</tspan> <tspan id="tspan5056" x="585" y="772" sodipodi:role="line">S. Hanna</tspan> <tspan id="tspan5058" x="585" y="778" sodipodi:role="line">F. Mao</tspan> <tspan id="tspan5060" x="585" y="784" sodipodi:role="line">S. McCamant</tspan> <tspan id="tspan5062" x="585" y="790" sodipodi:role="line">D. Song</tspan>
    </text>
    <text id="text4235" x="495" y="770" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan4239" x="495" y="770" sodipodi:role="line">M. Veanes</tspan> <tspan id="tspan4243" x="495" y="776" sodipodi:role="line">P. Halleux</tspan> <tspan id="tspan4245" x="495" y="782" sodipodi:role="line">N. Tillmann</tspan>
    </text>
    <text id="text4279" x="215" y="710" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan4283" x="215" y="710" sodipodi:role="line">A. Kieżun (M)</tspan> <tspan id="tspan4287" x="215" y="716" sodipodi:role="line">V. Ganesh (M)</tspan> <tspan id="tspan4289" x="215" y="722" sodipodi:role="line">P. J. Guo (S), ...</tspan>
    </text>
    <text id="text5210" x="105" y="850" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan5212" x="105" y="850" sodipodi:role="line">C. Barrett</tspan> <tspan id="tspan4529" x="105" y="856" sodipodi:role="line">...</tspan>
    </text>
    <text id="text5300" x="825" y="855" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan5308" x="825" y="855" sodipodi:role="line">W. Visser (S)</tspan> <tspan id="tspan5319" x="825" y="861" sodipodi:role="line">J. Geldenhuys (S)</tspan> <tspan id="tspan5321" x="825" y="867" sodipodi:role="line">M. B. Dwyer (N)</tspan>
    </text>
    <text id="text12932" x="105" y="1045" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan12934" x="105" y="1045" sodipodi:role="line">T. Liang (I), ...</tspan>
    </text>
    <text id="text12954" x="215" y="425" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan12956" x="215" y="425" sodipodi:role="line">A. Stump</tspan> <tspan id="tspan12962" x="215" y="431" sodipodi:role="line">C. W. Barrett, ...</tspan>
    </text>
    <text id="text12974" x="215" y="515" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan12978" x="215" y="515" sodipodi:role="line">C. W. Barrett (N)</tspan> <tspan id="tspan12980" x="215" y="521" sodipodi:role="line">S. Berezin (S)</tspan>
    </text>
    <text id="text13002" x="105" y="635" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan13004" x="105" y="635" sodipodi:role="line">C. Barrett (NY)</tspan> <tspan id="tspan13011" x="105" y="641" sodipodi:role="line">C. Tinelli (I)</tspan>
    </text>
    <text id="text13024" x="215" y="345" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan13028" x="215" y="345" sodipodi:role="line">C. W. Barrett</tspan> <tspan id="tspan13030" x="215" y="351" sodipodi:role="line">D. L. Dill</tspan> <tspan id="tspan13034" x="215" y="357" sodipodi:role="line">J. Levitt</tspan>
    </text>
    <text id="text4584" x="965" y="1122.5" font-size="6" overflow="visible" style="text-indent:0;text-align:end;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" text-anchor="end" sodipodi:linespacing="100%">
      <tspan id="tspan4596" x="965" y="1122.5" sodipodi:role="line">Sergey Vartanov and GitHub contributors, 2017</tspan>
    </text>
    <text id="text4598" x="965" y="1130" font-family="Fira Code" font-size="5" overflow="visible" style="text-indent:0;text-align:end;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Fira Code Light" text-anchor="end" sodipodi:linespacing="100%">
      <tspan id="tspan4604" x="965" y="1130" sodipodi:role="line">github.com/enzet/symbolic-execution</tspan>
    </text>
    <text id="text5562" x="495" y="555" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan5564" x="495" y="555" sodipodi:role="line">B. Dutertre</tspan> <tspan id="tspan5574" x="495" y="561" sodipodi:role="line">L. de Moura</tspan>
    </text>
    <text id="text5586" x="215" y="542.5" font-size="10" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" text-anchor="middle" sodipodi:linespacing="100%">
      <tspan id="tspan5588" x="215" y="542.5" font-size="6" style="text-align:center;-inkscape-font-specification:Roboto Light" sodipodi:role="line">C. W. Barrett</tspan>
    </text>
    <text id="text5594" x="544.461" y="577.5" font-size="10" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan5596" x="544.461" y="577.5" font-size="6" style="text-align:start;-inkscape-font-specification:Roboto Light" sodipodi:role="line">L. de Moura</tspan>
    </text>
    <text id="text4797" x="654.382" y="904.964" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan4801" x="654.382" y="904.964" sodipodi:role="line">E. Torlak</tspan> <tspan id="tspan4805" x="654.382" y="910.964" sodipodi:role="line">R. Bodik</tspan>
    </text>
    <text id="text6020" x="745" y="710" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan6024" x="745" y="710" sodipodi:role="line">R. Brummayer</tspan> <tspan id="tspan6028" x="745" y="716" sodipodi:role="line">A. Biere</tspan>
    </text>
    <text id="text6050" x="825" y="710" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan6052" x="825" y="710" sodipodi:role="line">N. Sörensson</tspan> <tspan id="tspan6054" x="825" y="716" sodipodi:role="line">A. Biere</tspan>
    </text>
    <text id="text6086" x="745" y="950" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan6090" x="745" y="950" sodipodi:role="line">C. Reisenberger</tspan>
    </text>
    <text id="text6111" x="745" y="1015" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan6115" x="745" y="1015" sodipodi:role="line">A. Niemetz</tspan> <tspan id="tspan6121" x="745" y="1021" sodipodi:role="line">M. Preiner</tspan> <tspan id="tspan6119" x="745" y="1027" sodipodi:role="line">A. Biere</tspan>
    </text>
    <text id="text5726" x="525.982" y="404.781" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan5730" x="525.982" y="404.781" sodipodi:role="line">M. W. Moskewicz (B)</tspan> <tspan id="tspan5736" x="525.982" y="410.781" sodipodi:role="line">C. F. Madigan (M)</tspan> <tspan id="tspan5742" x="525.982" y="416.781" sodipodi:role="line">Ying Zhao (P)</tspan> <tspan id="tspan13495" x="525.982" y="422.781" sodipodi:role="line">Lintao Zhang (P), ... (P)</tspan>
    </text>
    <text id="text5778" x="135" y="355" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan5784" x="135" y="355" sodipodi:role="line">J. P. M. Silva (C)</tspan> <tspan id="tspan5791" x="135" y="361" sodipodi:role="line">K. A. Sakallah (M)</tspan>
    </text>
    <text id="text5813" x="895" y="440" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan5815" x="895" y="440" sodipodi:role="line">N. Eén</tspan> <tspan id="tspan5817" x="895" y="446" sodipodi:role="line">N. Sörensson</tspan>
    </text>
    <text id="text13558" x="305" y="360" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan13562" x="305" y="360" sodipodi:role="line">Hantao Zhang</tspan>
    </text>
    <text id="text13599" x="215.982" y="249.781" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan13607" x="215.982" y="249.781" sodipodi:role="line">M. Davis</tspan> <tspan id="tspan13618" x="215.982" y="255.781" sodipodi:role="line">H. Putnam</tspan>
    </text>
    <text id="text13651" x="305.982" y="249.781" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan13653" x="305.982" y="249.781" sodipodi:role="line">M. Davis</tspan> <tspan id="tspan13655" x="305.982" y="255.781" sodipodi:role="line">H. Putnam</tspan> <tspan id="tspan13663" x="305.982" y="261.781" sodipodi:role="line">G. Logeman</tspan> <tspan id="tspan13659" x="305.982" y="267.781" sodipodi:role="line">D. Loveland</tspan>
    </text>
    <text id="text15891" x="65" y="330" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan15895" x="65" y="330" sodipodi:role="line">B. Selman (C)</tspan> <tspan id="tspan15906" x="65" y="336" sodipodi:role="line">H. Kautz (R)</tspan> <tspan id="tspan15908" x="65" y="342" sodipodi:role="line">B. Cohen</tspan>
    </text>
    <text id="text15938" x="375" y="365" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan15942" x="375" y="365" sodipodi:role="line">R. Paturi</tspan> <tspan id="tspan16465" x="375" y="371" sodipodi:role="line">P. Pudlák</tspan> <tspan id="tspan16467" x="375" y="377" sodipodi:role="line">F. Zane</tspan>
    </text>
    <text id="text16493" x="445" y="370" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan16495" x="445" y="370" sodipodi:role="line">R. Paturi</tspan> <tspan id="tspan16497" x="445" y="376" sodipodi:role="line">P. Pudlák</tspan> <tspan id="tspan16501" x="445" y="382" sodipodi:role="line">E. Saks</tspan> <tspan id="tspan16499" x="445" y="388" sodipodi:role="line">F. Zane</tspan>
    </text>
    <text id="text13798" x="106.967" y="559.781" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan13800" x="106.967" y="559.781" sodipodi:role="line">S. Rainse (Na.)</tspan> <tspan id="tspan13802" x="106.967" y="565.781" sodipodi:role="line">C. Tinelli (I)</tspan>
    </text>
    <text id="text13822" x="105" y="760" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan13824" x="105" y="760" sodipodi:role="line">C. Barrett (NY)</tspan> <tspan id="tspan13828" x="105" y="766" sodipodi:role="line">A. Stump</tspan> <tspan id="tspan13826" x="105" y="772" sodipodi:role="line">C. Tinelli (I)</tspan>
    </text>
    <text id="text3561" x="295" y="1090" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan3563" x="295" y="1090" sodipodi:role="line">M. Berzish (W)</tspan> <tspan id="tspan3565" x="295" y="1096" sodipodi:role="line">Y. Zheng (I)</tspan> <tspan id="tspan3569" x="295" y="1102" sodipodi:role="line">V. Ganesh (W)</tspan>
    </text>
    <text id="text3614" x="285" y="1015" font-size="6" overflow="visible" style="text-indent:0;text-align:center;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" text-anchor="middle" sodipodi:linespacing="100%">
      <tspan id="tspan3616" x="285" y="1015" sodipodi:role="line">Y. Zheng</tspan>
    </text>
    <text id="text3569" x="345" y="1090" font-size="6" font-style="italic" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light Italic" sodipodi:linespacing="100%">
      <tspan id="tspan3571" x="345" y="1090" sodipodi:role="line">As part of Z3</tspan>
    </text>
    <text id="text3574" x="895" y="945" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan3578" x="895" y="945" sodipodi:role="line">P. A. Abdulla (U)</tspan> <tspan id="tspan3604" x="895" y="951" sodipodi:role="line">M. F. Atig (U)</tspan> <tspan id="tspan3606" x="895" y="957" sodipodi:role="line">Yu-Fang Chen (S)</tspan> <tspan id="tspan3608" x="895" y="963" sodipodi:role="line">L. Holík (B)</tspan>
    </text>
    <text id="text3593" x="395" y="970" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan3595" x="395" y="970" sodipodi:role="line">Minh-Tai Trinh</tspan> <tspan id="tspan3599" x="395" y="976" sodipodi:role="line">Duc-Hiep Chu</tspan> <tspan id="tspan3601" x="395" y="982" sodipodi:role="line">J. Jaffar</tspan>
    </text>
    <text id="text3645" x="395" y="1070" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan3647" x="395" y="1070" sodipodi:role="line">Minh-Tai Trinh</tspan> <tspan id="tspan3649" x="395" y="1076" sodipodi:role="line">Duc-Hiep Chu</tspan> <tspan id="tspan3651" x="395" y="1082" sodipodi:role="line">J. Jaffar</tspan>
    </text>
    <text id="text3636" x="586.529" y="1019.324" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan3642" x="586.529" y="1019.324" sodipodi:role="line">A. Aydin</tspan> <tspan id="tspan3659" x="586.529" y="1025.324" sodipodi:role="line">L. Bang</tspan> <tspan id="tspan3661" x="586.529" y="1031.324" sodipodi:role="line">T. Bultan</tspan>
    </text>
    <text id="text3681" x="395.866" y="723.941" font-size="6" overflow="visible" style="text-indent:0;text-align:start;line-height:100%;text-transform:none;block-progression:tb;marker:none;-inkscape-font-specification:Roboto Light" sodipodi:linespacing="100%">
      <tspan id="tspan3687" x="395.866" y="723.941" sodipodi:role="line">P. Hooimeijer</tspan> <tspan id="tspan3703" x="395.866" y="729.941" sodipodi:role="line">W. Weimer</tspan>
    </text>
  </g>
  <g id="g2096" transform="translate(-80 -185)" inkscape:label="preview">
    <rect id="rect2098" width="305" height="240" x="280" y="180" fill="none" rx="0" ry="0" inkscape:groupmode="layer" inkscape:label="#rect4031"/>
  </g>
</svg>