CORE symex-driven-lazy-loading-expected-failure
My.class
--function "My.<init>" --nondet-static --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
^EXIT=10$
^SIGNAL=0$
file My\.java line 104 function java::My\.\<init\>:\(I\)V.*FAILURE$
file My\.java line 106 function java::My\.\<init\>:\(I\)V.*FAILURE$
file My\.java line 108 function java::My\.\<init\>:\(I\)V.*FAILURE$
file My\.java line 110 function java::My\.\<init\>:\(I\)V.*FAILURE$
file My\.java line 112 function java::My\.\<init\>:\(I\)V.*FAILURE$
file My\.java line 117 function java::My\.\<init\>:\(I\)V.*SUCCESS$
file My\.java line 119 function java::My\.\<init\>:\(I\)V.*SUCCESS$
file My\.java line 121 function java::My\.\<init\>:\(I\)V.*SUCCESS$
file My\.java line 124 function java::My\.\<init\>:\(I\)V.*FAILURE$
file My\.java line 126 function java::My\.\<init\>:\(I\)V.*FAILURE$
file My\.java line 128 function java::My\.\<init\>:\(I\)V.*FAILURE$
file My\.java line 130 function java::My\.\<init\>:\(I\)V.*FAILURE$
file My\.java line 132 function java::My\.\<init\>:\(I\)V.*FAILURE$
file My\.java line 137 function java::My\.\<init\>:\(I\)V.*SUCCESS$
file My\.java line 139 function java::My\.\<init\>:\(I\)V.*SUCCESS$
file My\.java line 141 function java::My\.\<init\>:\(I\)V.*SUCCESS$
file My\.java line 150 function java::My\.\<init\>:\(I\)V.*FAILURE$
file My\.java line 152 function java::My\.\<init\>:\(I\)V.*FAILURE$
file My\.java line 154 function java::My\.\<init\>:\(I\)V.*FAILURE$
file My\.java line 156 function java::My\.\<init\>:\(I\)V.*FAILURE$
file My\.java line 158 function java::My\.\<init\>:\(I\)V.*FAILURE$
file My\.java line 163 function java::My\.\<init\>:\(I\)V.*SUCCESS$
file My\.java line 165 function java::My\.\<init\>:\(I\)V.*SUCCESS$
file My\.java line 167 function java::My\.\<init\>:\(I\)V.*SUCCESS$
file My\.java line 170 function java::My\.\<init\>:\(I\)V.*FAILURE$
file My\.java line 172 function java::My\.\<init\>:\(I\)V.*FAILURE$
file My\.java line 174 function java::My\.\<init\>:\(I\)V.*FAILURE$
file My\.java line 176 function java::My\.\<init\>:\(I\)V.*FAILURE$
file My\.java line 178 function java::My\.\<init\>:\(I\)V.*FAILURE$
file My\.java line 183 function java::My\.\<init\>:\(I\)V.*SUCCESS$
file My\.java line 185 function java::My\.\<init\>:\(I\)V.*SUCCESS$
file My\.java line 187 function java::My\.\<init\>:\(I\)V.*SUCCESS$
file My\.java line 196 function java::My\.\<init\>:\(I\)V.*FAILURE$
file My\.java line 198 function java::My\.\<init\>:\(I\)V.*FAILURE$
file My\.java line 200 function java::My\.\<init\>:\(I\)V.*FAILURE$
file My\.java line 202 function java::My\.\<init\>:\(I\)V.*FAILURE$
file My\.java line 204 function java::My\.\<init\>:\(I\)V.*FAILURE$
file My\.java line 209 function java::My\.\<init\>:\(I\)V.*SUCCESS$
file My\.java line 211 function java::My\.\<init\>:\(I\)V.*SUCCESS$
file My\.java line 213 function java::My\.\<init\>:\(I\)V.*SUCCESS$
file My\.java line 216 function java::My\.\<init\>:\(I\)V.*FAILURE$
file My\.java line 218 function java::My\.\<init\>:\(I\)V.*FAILURE$
file My\.java line 220 function java::My\.\<init\>:\(I\)V.*FAILURE$
file My\.java line 222 function java::My\.\<init\>:\(I\)V.*FAILURE$
file My\.java line 224 function java::My\.\<init\>:\(I\)V.*FAILURE$
file My\.java line 229 function java::My\.\<init\>:\(I\)V.*SUCCESS$
file My\.java line 231 function java::My\.\<init\>:\(I\)V.*SUCCESS$
file My\.java line 233 function java::My\.\<init\>:\(I\)V.*SUCCESS$
file My\.java line 236 function java::My\.\<init\>:\(I\)V.*SUCCESS$
--
file My\.java line 115 function java::My\.\<init\>:\(I\)V
file My\.java line 135 function java::My\.\<init\>:\(I\)V
file My\.java line 144 function java::My\.\<init\>:\(I\)V
file My\.java line 147 function java::My\.\<init\>:\(I\)V
file My\.java line 161 function java::My\.\<init\>:\(I\)V
file My\.java line 181 function java::My\.\<init\>:\(I\)V
file My\.java line 190 function java::My\.\<init\>:\(I\)V
file My\.java line 193 function java::My\.\<init\>:\(I\)V
file My\.java line 207 function java::My\.\<init\>:\(I\)V
file My\.java line 227 function java::My\.\<init\>:\(I\)V
--
This tests nondet-static option

This fails under symex-driven lazy loading because nondet-static cannot be used
with it
