| benchmark name | SwInE Z3 | SwInE Legacy | SwInE Z3 no rewriting | SwInE Z3 no symmetry | SwInE Z3 no monotonicity | SwInE Z3 no bounding | SwInE Z3 no prime | SwInE Z3 no induction | SwInE Z3 no interpolation | SwInE Z3 no phasing |
|---|
| chc-LIA-Lin_060.smt2_0.smt2 | sat (0.397) | sat (0.822) | sat (0.404) | sat (0.395) | sat (0.408) | unknown (0.460) | sat (0.404) | sat (0.397) | sat (0.405) | sat (0.452) |
| chc-LIA-Lin_060.smt2_1.smt2 | sat (0.389) | sat (0.553) | sat (0.404) | sat (0.403) | sat (0.419) | unknown (0.488) | sat (0.391) | sat (0.397) | sat (0.403) | sat (0.702) |
| chc-LIA-Lin_060.smt2_2.smt2 | sat (0.407) | sat (0.500) | sat (0.412) | sat (0.401) | sat (0.410) | unknown (0.473) | sat (0.407) | sat (0.403) | sat (0.405) | sat (0.444) |
| chc-LIA-Lin_060.smt2_3.smt2 | sat (0.416) | sat (0.522) | sat (0.397) | sat (0.394) | sat (0.419) | unknown (0.515) | sat (0.396) | sat (0.402) | sat (0.401) | sat (0.433) |
| chc-LIA-Lin_060.smt2_4.smt2 | sat (0.357) | sat (0.521) | sat (0.400) | sat (0.395) | sat (0.408) | unknown (0.444) | sat (0.399) | sat (0.418) | sat (0.441) | sat (0.657) |
| chc-LIA-Lin_060.smt2_6.smt2 | sat (0.424) | sat (0.789) | sat (0.404) | sat (0.386) | sat (0.406) | unknown (0.446) | sat (0.477) | sat (0.416) | sat (0.432) | sat (0.408) |
| chc-LIA-Lin_093.smt2_0.smt2 | sat (0.401) | sat (0.560) | sat (0.393) | sat (0.373) | sat (0.402) | sat (0.379) | sat (0.396) | sat (0.387) | unknown (0.400) | sat (0.442) |
| chc-LIA-Lin_272.smt2_0.smt2 | unsat (0.448) | unsat (0.625) | unsat (0.358) | unsat (0.411) | unsat (0.416) | unsat (0.389) | unsat (0.427) | unsat (0.396) | unsat (0.446) | unsat (0.429) |
| chc-LIA-Lin_272.smt2_1.smt2 | sat (0.423) | sat (0.574) | sat (0.409) | sat (0.410) | sat (0.406) | sat (0.386) | sat (0.457) | sat (0.400) | unknown (0.449) | sat (0.408) |
| chc-LIA-Lin_272.smt2_2.smt2 | unsat (0.513) | unsat (0.626) | unsat (0.392) | unsat (0.406) | unsat (0.404) | unsat (0.401) | unsat (0.438) | unsat (0.402) | unsat (0.452) | unsat (0.385) |
| chc-LIA-Lin_272.smt2_3.smt2 | unsat (0.424) | unsat (0.541) | unsat (0.419) | unsat (0.364) | unsat (0.397) | unsat (0.391) | unsat (0.394) | unsat (0.409) | unsat (0.406) | unsat (0.404) |
| chc-LIA-Lin_273.smt2_0.smt2 | sat (0.427) | sat (0.530) | sat (0.425) | sat (0.411) | sat (0.411) | unknown (0.517) | sat (0.549) | sat (0.474) | unknown (0.432) | sat (0.445) |
| chc-LIA-Lin_273.smt2_1.smt2 | unsat (0.439) | unsat (0.508) | unsat (0.385) | unsat (0.387) | unsat (0.394) | unsat (0.368) | unsat (0.405) | unsat (0.411) | unsat (0.406) | unsat (0.405) |
| chc-LIA-Lin_273.smt2_2.smt2 | sat (0.411) | sat (0.545) | sat (0.374) | sat (0.383) | sat (0.411) | unknown (0.447) | sat (0.404) | sat (0.400) | sat (0.419) | sat (0.437) |
| chc-LIA-Lin_273.smt2_3.smt2 | unsat (0.417) | unsat (0.503) | unsat (0.382) | unsat (0.456) | unsat (0.384) | unsat (0.408) | unsat (0.376) | unsat (0.394) | unsat (0.429) | unsat (0.404) |
| chc-LIA-Lin_273.smt2_4.smt2 | unsat (0.429) | unsat (0.509) | unsat (0.389) | unsat (0.396) | unsat (0.396) | unsat (0.440) | unsat (0.396) | unsat (0.402) | unsat (0.437) | unsat (0.412) |
| chc-LIA-Lin_277.smt2_0.smt2 | sat (0.457) | sat (0.552) | sat (0.401) | sat (0.408) | sat (0.396) | sat (0.398) | sat (0.413) | sat (0.366) | sat (0.614) | sat (0.432) |
| chc-LIA-Lin_277.smt2_1.smt2 | unsat (0.412) | unsat (0.510) | unsat (0.403) | unsat (0.376) | unsat (0.322) | unsat (0.430) | unsat (0.436) | unsat (0.366) | unsat (0.349) | unsat (0.383) |
| chc-LIA-Lin_277.smt2_10.smt2 | sat (0.494) | sat (0.528) | sat (0.470) | sat (0.476) | sat (0.466) | sat (0.467) | sat (0.601) | sat (0.476) | sat (0.500) | sat (0.438) |
| chc-LIA-Lin_277.smt2_11.smt2 | unsat (0.596) | unsat (0.527) | unsat (0.465) | unsat (0.500) | unsat (0.450) | unsat (0.475) | unsat (0.474) | unsat (0.476) | unsat (0.437) | unsat (0.410) |
| chc-LIA-Lin_277.smt2_13.smt2 | unsat (0.495) | unsat (0.524) | unsat (0.427) | unsat (0.472) | unsat (0.453) | unsat (0.449) | unsat (0.483) | unsat (0.542) | unsat (0.487) | unsat (0.486) |
| chc-LIA-Lin_277.smt2_14.smt2 | sat (0.461) | sat (0.529) | sat (0.415) | sat (0.420) | sat (0.400) | sat (0.415) | sat (0.461) | sat (0.458) | sat (0.444) | sat (0.428) |
| chc-LIA-Lin_277.smt2_16.smt2 | unsat (0.427) | unsat (0.537) | unsat (0.406) | unsat (0.442) | unsat (0.386) | unsat (0.407) | unsat (0.408) | unsat (0.428) | unsat (0.424) | unsat (0.418) |
| chc-LIA-Lin_277.smt2_17.smt2 | sat (0.423) | sat (0.555) | sat (0.455) | sat (0.414) | sat (0.410) | sat (0.412) | sat (0.436) | sat (0.491) | sat (0.457) | sat (0.460) |
| chc-LIA-Lin_277.smt2_18.smt2 | sat (0.427) | sat (0.534) | sat (0.409) | sat (0.402) | sat (0.412) | sat (0.433) | sat (0.561) | sat (0.413) | sat (0.641) | sat (0.425) |
| chc-LIA-Lin_277.smt2_19.smt2 | unsat (0.439) | unsat (0.541) | unsat (0.410) | unsat (0.403) | unsat (0.426) | unsat (0.432) | unsat (0.442) | unsat (0.402) | unsat (0.433) | unsat (0.424) |
| chc-LIA-Lin_277.smt2_2.smt2 | sat (0.397) | sat (0.538) | sat (0.395) | sat (0.483) | sat (0.414) | sat (0.397) | sat (0.423) | sat (0.397) | sat (0.403) | sat (0.439) |
| chc-LIA-Lin_277.smt2_20.smt2 | sat (0.364) | sat (0.534) | sat (0.411) | sat (0.424) | sat (0.412) | sat (0.409) | sat (0.562) | sat (0.430) | sat (0.436) | sat (0.422) |
| chc-LIA-Lin_277.smt2_22.smt2 | sat (0.449) | sat (0.548) | sat (0.412) | sat (0.472) | sat (0.421) | sat (0.442) | sat (0.542) | sat (0.380) | sat (0.424) | sat (0.400) |
| chc-LIA-Lin_277.smt2_23.smt2 | sat (0.423) | sat (0.558) | sat (0.401) | sat (0.399) | sat (0.426) | sat (0.422) | sat (0.549) | sat (0.370) | sat (0.456) | sat (0.428) |
| chc-LIA-Lin_277.smt2_24.smt2 | unsat (0.428) | unsat (0.547) | unsat (0.393) | unsat (0.392) | unsat (0.426) | unsat (0.409) | unsat (0.449) | unsat (0.412) | unsat (0.430) | unsat (0.424) |
| chc-LIA-Lin_277.smt2_25.smt2 | sat (0.476) | sat (0.527) | sat (0.449) | sat (0.393) | sat (0.426) | sat (0.433) | sat (0.449) | sat (0.421) | sat (0.365) | sat (0.401) |
| chc-LIA-Lin_277.smt2_27.smt2 | unsat (0.453) | unsat (0.498) | unsat (0.406) | unsat (0.369) | unsat (0.399) | unsat (0.438) | unsat (0.422) | unsat (0.384) | unsat (0.416) | unsat (0.391) |
| chc-LIA-Lin_277.smt2_28.smt2 | unsat (0.391) | unsat (0.502) | unsat (0.389) | unsat (0.536) | unsat (0.400) | unsat (0.390) | unsat (0.400) | unsat (0.387) | unsat (0.388) | unsat (0.423) |
| chc-LIA-Lin_277.smt2_29.smt2 | unsat (0.393) | unsat (0.500) | unsat (0.397) | unsat (0.529) | unsat (0.404) | unsat (0.406) | unsat (0.397) | unsat (0.387) | unsat (0.423) | unsat (0.413) |
| chc-LIA-Lin_277.smt2_3.smt2 | sat (0.411) | sat (0.519) | sat (0.408) | sat (0.527) | sat (0.470) | sat (0.399) | sat (0.411) | sat (0.413) | sat (0.365) | sat (0.420) |
| chc-LIA-Lin_277.smt2_30.smt2 | sat (0.345) | sat (0.539) | sat (0.401) | sat (0.561) | sat (0.413) | sat (0.402) | sat (0.409) | sat (0.399) | sat (0.401) | sat (0.446) |
| chc-LIA-Lin_277.smt2_31.smt2 | sat (0.337) | sat (0.559) | sat (0.416) | sat (0.381) | sat (0.411) | sat (0.407) | sat (0.435) | sat (0.409) | sat (0.409) | sat (0.467) |
| chc-LIA-Lin_277.smt2_32.smt2 | unsat (0.391) | unsat (0.511) | unsat (0.341) | unsat (0.400) | unsat (0.483) | unsat (0.404) | unsat (0.431) | unsat (0.388) | unsat (0.425) | unsat (0.312) |
| chc-LIA-Lin_277.smt2_35.smt2 | unsat (0.404) | unsat (0.506) | unsat (0.394) | unsat (0.527) | unsat (0.463) | unsat (0.392) | unsat (0.343) | unsat (0.395) | unsat (0.403) | unsat (0.393) |
| chc-LIA-Lin_277.smt2_4.smt2 | unsat (0.401) | unsat (0.570) | unsat (0.395) | unsat (0.489) | unsat (0.365) | unsat (0.391) | unsat (0.400) | unsat (0.391) | unsat (0.386) | unsat (0.384) |
| chc-LIA-Lin_277.smt2_5.smt2 | sat (0.399) | sat (0.597) | sat (0.399) | sat (0.480) | sat (0.421) | sat (0.394) | sat (0.424) | sat (0.402) | sat (0.374) | sat (0.598) |
| chc-LIA-Lin_277.smt2_6.smt2 | sat (0.400) | sat (0.570) | sat (0.388) | sat (0.472) | sat (0.398) | sat (0.392) | sat (0.405) | sat (0.397) | sat (0.424) | sat (0.464) |
| chc-LIA-Lin_277.smt2_7.smt2 | sat (0.373) | sat (0.560) | sat (0.431) | sat (0.481) | sat (0.394) | sat (0.364) | sat (0.416) | sat (0.408) | sat (0.405) | sat (0.471) |
| chc-LIA-Lin_277.smt2_8.smt2 | unsat (0.461) | unsat (0.538) | unsat (0.423) | unsat (0.406) | unsat (0.398) | unsat (0.404) | unsat (0.395) | unsat (0.374) | unsat (0.397) | unsat (0.416) |
| chc-LIA-Lin_277.smt2_9.smt2 | sat (0.369) | sat (0.516) | sat (0.402) | sat (0.392) | sat (0.405) | sat (0.401) | sat (0.395) | sat (0.412) | sat (0.400) | sat (0.458) |
| chc-LIA-Lin_278.smt2_0.smt2 | sat (0.407) | sat (0.607) | sat (0.415) | sat (0.425) | sat (0.413) | sat (0.398) | sat (0.411) | sat (0.412) | unknown (0.427) | sat (0.459) |
| chc-LIA-Lin_278.smt2_1.smt2 | unsat (0.473) | unsat (0.506) | unsat (0.358) | unsat (0.543) | unsat (0.425) | unsat (0.366) | unsat (0.404) | unsat (0.444) | unsat (0.404) | unsat (0.551) |
| chc-LIA-Lin_278.smt2_10.smt2 | sat (0.405) | sat (0.604) | sat (0.428) | sat (0.421) | sat (0.416) | sat (0.404) | sat (0.424) | sat (0.397) | unknown (0.375) | sat (0.459) |
| chc-LIA-Lin_278.smt2_11.smt2 | unsat (0.403) | unsat (0.544) | unsat (0.394) | unsat (0.480) | unsat (0.362) | unsat (0.344) | unsat (0.418) | unsat (0.389) | unsat (0.394) | unsat (0.450) |
| chc-LIA-Lin_278.smt2_14.smt2 | sat (0.451) | sat (0.577) | sat (0.505) | sat (0.570) | sat (0.393) | sat (0.432) | sat (0.452) | sat (0.507) | unknown (0.494) | sat (0.593) |
| chc-LIA-Lin_278.smt2_15.smt2 | unsat (0.488) | unsat (0.565) | unsat (0.563) | unsat (0.522) | unsat (0.471) | unsat (0.494) | unsat (0.570) | unsat (0.556) | unsat (0.564) | unsat (0.706) |
| chc-LIA-Lin_278.smt2_16.smt2 | sat (0.430) | sat (0.554) | sat (0.472) | sat (0.549) | sat (0.444) | sat (0.476) | sat (0.555) | sat (0.541) | unknown (0.504) | sat (0.581) |
| chc-LIA-Lin_278.smt2_17.smt2 | sat (0.440) | sat (0.622) | sat (0.440) | sat (0.406) | sat (0.455) | sat (0.507) | sat (0.462) | sat (0.436) | unknown (0.490) | sat (0.477) |
| chc-LIA-Lin_278.smt2_18.smt2 | unsat (0.527) | unsat (0.602) | unsat (0.544) | unsat (0.537) | unsat (0.589) | unsat (0.656) | unsat (0.560) | unsat (0.558) | unsat (0.570) | unsat (0.471) |
| chc-LIA-Lin_278.smt2_19.smt2 | sat (0.591) | sat (0.578) | sat (0.486) | sat (0.519) | sat (0.520) | sat (0.573) | sat (0.407) | sat (0.507) | unknown (0.508) | sat (0.495) |
| chc-LIA-Lin_278.smt2_2.smt2 | sat (0.418) | sat (0.616) | sat (0.434) | sat (0.417) | sat (0.393) | sat (0.412) | sat (0.403) | sat (0.409) | unknown (0.402) | sat (0.438) |
| chc-LIA-Lin_278.smt2_20.smt2 | sat (0.546) | sat (0.597) | sat (0.420) | sat (0.463) | sat (0.430) | sat (0.451) | sat (0.453) | sat (0.457) | unknown (0.404) | sat (0.465) |
| chc-LIA-Lin_278.smt2_21.smt2 | unsat (0.405) | unsat (0.487) | unsat (0.403) | unsat (0.419) | unsat (0.350) | unsat (0.433) | unsat (0.405) | unsat (0.403) | unsat (0.392) | unsat (0.528) |
| chc-LIA-Lin_278.smt2_22.smt2 | sat (0.432) | sat (0.626) | sat (0.436) | sat (0.408) | sat (0.424) | sat (0.445) | sat (0.457) | sat (0.448) | unknown (0.420) | sat (0.491) |
| chc-LIA-Lin_278.smt2_23.smt2 | sat (0.441) | sat (0.624) | sat (0.434) | sat (0.430) | sat (0.433) | sat (0.440) | sat (0.522) | sat (0.439) | unknown (0.422) | sat (0.626) |
| chc-LIA-Lin_278.smt2_24.smt2 | unsat (0.534) | unsat (0.586) | unsat (0.525) | unsat (0.500) | unsat (0.467) | unsat (0.491) | unsat (0.494) | unsat (0.519) | unsat (0.491) | unsat (0.449) |
| chc-LIA-Lin_278.smt2_27.smt2 | unsat (0.396) | unsat (0.525) | unsat (0.450) | unsat (0.410) | unsat (0.357) | unsat (0.358) | unsat (0.406) | unsat (0.409) | unsat (0.378) | unsat (0.403) |
| chc-LIA-Lin_278.smt2_28.smt2 | unsat (0.525) | unsat (0.544) | unsat (0.442) | unsat (0.330) | unsat (0.379) | unsat (0.398) | unsat (0.407) | unsat (0.408) | unsat (0.411) | unsat (0.411) |
| chc-LIA-Lin_278.smt2_29.smt2 | unsat (0.435) | unsat (0.497) | unsat (0.447) | unsat (0.439) | unsat (0.393) | unsat (0.414) | unsat (0.399) | unsat (0.393) | unsat (0.401) | unsat (0.427) |
| chc-LIA-Lin_278.smt2_3.smt2 | sat (0.417) | sat (0.521) | sat (0.413) | sat (0.405) | sat (0.479) | sat (0.405) | sat (0.390) | sat (0.389) | unknown (0.399) | sat (0.410) |
| chc-LIA-Lin_278.smt2_30.smt2 | sat (0.423) | sat (0.614) | sat (0.427) | sat (0.395) | sat (0.405) | sat (0.408) | sat (0.400) | sat (0.417) | unknown (0.405) | sat (0.462) |
| chc-LIA-Lin_278.smt2_31.smt2 | sat (0.375) | sat (0.573) | sat (0.436) | sat (0.407) | sat (0.355) | sat (0.355) | sat (0.408) | sat (0.407) | unknown (0.402) | sat (0.454) |
| chc-LIA-Lin_278.smt2_32.smt2 | unsat (0.407) | unsat (0.567) | unsat (0.404) | unsat (0.411) | unsat (0.393) | unsat (0.392) | unsat (0.403) | unsat (0.385) | unsat (0.401) | unsat (0.426) |
| chc-LIA-Lin_278.smt2_35.smt2 | unsat (0.402) | unsat (0.506) | unsat (0.367) | unsat (0.374) | unsat (0.398) | unsat (0.431) | unsat (0.388) | unsat (0.388) | unsat (0.393) | unsat (0.356) |
| chc-LIA-Lin_278.smt2_4.smt2 | unsat (0.395) | unsat (0.576) | unsat (0.394) | unsat (0.389) | unsat (0.408) | unsat (0.393) | unsat (0.378) | unsat (0.378) | unsat (0.393) | unsat (0.404) |
| chc-LIA-Lin_278.smt2_5.smt2 | sat (0.409) | sat (0.604) | sat (0.417) | sat (0.388) | sat (0.494) | sat (0.377) | sat (0.399) | sat (0.392) | unknown (0.396) | sat (0.425) |
| chc-LIA-Lin_278.smt2_6.smt2 | sat (0.422) | sat (0.580) | sat (0.415) | sat (0.397) | sat (0.424) | sat (0.391) | sat (0.406) | sat (0.404) | unknown (0.391) | sat (0.412) |
| chc-LIA-Lin_278.smt2_8.smt2 | unsat (0.401) | unsat (0.568) | unsat (0.381) | unsat (0.390) | unsat (0.518) | unsat (0.383) | unsat (0.386) | unsat (0.382) | unsat (0.392) | unsat (0.402) |
| chc-LIA-Lin_278.smt2_9.smt2 | sat (0.412) | sat (0.573) | sat (0.426) | sat (0.399) | sat (0.408) | sat (0.386) | sat (0.387) | sat (0.390) | unknown (0.398) | sat (0.460) |
| chc-LIA-Lin_279.smt2_0.smt2 | sat (0.395) | sat (0.522) | sat (0.422) | sat (0.400) | sat (0.421) | sat (0.388) | sat (0.379) | sat (0.382) | unknown (0.385) | sat (0.443) |
| chc-LIA-Lin_279.smt2_1.smt2 | unsat (0.412) | unsat (0.459) | unsat (0.394) | unsat (0.405) | unsat (0.397) | unsat (0.397) | unsat (0.399) | unsat (0.398) | unsat (0.401) | unsat (0.406) |
| chc-LIA-Lin_279.smt2_11.smt2 | unsat (0.386) | unsat (0.556) | unsat (0.385) | unsat (0.378) | unsat (0.391) | unsat (0.381) | unsat (0.396) | unsat (0.378) | unsat (0.378) | unsat (0.420) |
| chc-LIA-Lin_279.smt2_12.smt2 | sat (0.396) | sat (0.598) | sat (0.417) | sat (0.382) | sat (0.370) | sat (0.380) | sat (0.396) | sat (0.395) | unknown (0.391) | sat (0.443) |
| chc-LIA-Lin_279.smt2_13.smt2 | sat (0.386) | sat (0.570) | sat (0.405) | sat (0.394) | sat (0.404) | sat (0.373) | sat (0.404) | sat (0.391) | unknown (0.390) | sat (0.438) |
| chc-LIA-Lin_279.smt2_14.smt2 | unsat (0.396) | unsat (0.535) | unsat (0.369) | unsat (0.396) | unsat (0.398) | unsat (0.367) | unsat (0.386) | unsat (0.389) | unsat (0.382) | unsat (0.419) |
| chc-LIA-Lin_279.smt2_15.smt2 | sat (0.430) | sat (0.519) | sat (0.432) | sat (0.626) | sat (0.437) | sat (0.433) | sat (0.417) | sat (0.433) | unknown (0.405) | sat (0.482) |
| chc-LIA-Lin_279.smt2_16.smt2 | sat (0.460) | sat (1.12) | sat (0.430) | sat (0.600) | sat (0.446) | sat (0.413) | sat (0.421) | sat (0.434) | unknown (0.411) | sat (0.444) |
| chc-LIA-Lin_279.smt2_17.smt2 | sat (0.435) | sat (1.8) | sat (0.439) | sat (0.608) | sat (0.429) | sat (0.425) | sat (0.427) | sat (0.444) | unknown (0.413) | sat (0.449) |
| chc-LIA-Lin_279.smt2_18.smt2 | unsat (0.751) | unsat (0.557) | unsat (0.709) | unsat (0.826) | unsat (0.758) | unsat (0.761) | unsat (0.736) | unsat (0.767) | unsat (0.744) | unsat (1.301) |
| chc-LIA-Lin_279.smt2_19.smt2 | sat (0.386) | sat (0.523) | sat (0.435) | sat (0.425) | sat (0.421) | sat (0.430) | sat (0.433) | sat (0.424) | unknown (0.425) | sat (0.499) |
| chc-LIA-Lin_279.smt2_2.smt2 | unsat (0.398) | unsat (0.526) | unsat (0.407) | unsat (0.405) | unsat (0.389) | unsat (0.396) | unsat (0.407) | unsat (0.397) | unsat (0.405) | unsat (0.439) |
| chc-LIA-Lin_279.smt2_20.smt2 | unsat (0.402) | unsat (0.556) | unsat (0.406) | unsat (0.404) | unsat (0.402) | unsat (0.361) | unsat (0.411) | unsat (0.399) | unsat (0.415) | unsat (0.405) |
| chc-LIA-Lin_279.smt2_22.smt2 | sat (0.452) | sat (0.559) | sat (0.384) | sat (0.434) | sat (0.445) | sat (0.430) | sat (0.434) | sat (0.397) | unknown (0.433) | sat (0.436) |
| chc-LIA-Lin_279.smt2_23.smt2 | sat (0.453) | sat (0.560) | sat (0.442) | sat (0.483) | sat (0.448) | sat (0.412) | sat (0.457) | sat (0.443) | unknown (0.447) | sat (0.448) |
| chc-LIA-Lin_279.smt2_24.smt2 | unsat (0.560) | unsat (0.636) | unsat (0.466) | unsat (0.464) | unsat (0.525) | unsat (0.545) | unsat (0.522) | unsat (0.550) | unsat (0.563) | unsat (0.440) |
| chc-LIA-Lin_279.smt2_26.smt2 | unsat (0.405) | unsat (0.535) | unsat (0.407) | unsat (0.405) | unsat (0.395) | unsat (0.404) | unsat (0.416) | unsat (0.406) | unsat (0.345) | unsat (0.435) |
| chc-LIA-Lin_279.smt2_27.smt2 | sat (0.440) | sat (0.565) | sat (0.417) | sat (0.384) | sat (0.403) | sat (0.405) | sat (0.406) | sat (0.406) | unknown (0.415) | sat (0.463) |
| chc-LIA-Lin_279.smt2_28.smt2 | sat (0.416) | sat (0.592) | sat (0.431) | sat (0.408) | sat (0.398) | sat (0.389) | sat (0.411) | sat (0.399) | unknown (0.419) | sat (0.462) |
| chc-LIA-Lin_279.smt2_29.smt2 | sat (0.425) | sat (0.553) | sat (0.410) | sat (0.428) | sat (0.388) | sat (0.410) | sat (0.397) | sat (0.407) | unknown (0.392) | sat (0.476) |
| chc-LIA-Lin_279.smt2_3.smt2 | sat (0.536) | sat (0.553) | sat (0.413) | sat (0.483) | sat (0.474) | sat (0.483) | sat (0.501) | sat (0.485) | unknown (0.484) | sat (0.571) |
| chc-LIA-Lin_279.smt2_30.smt2 | unsat (0.412) | unsat (0.513) | unsat (0.413) | unsat (0.357) | unsat (0.409) | unsat (0.392) | unsat (0.363) | unsat (0.409) | unsat (0.399) | unsat (0.433) |
| chc-LIA-Lin_279.smt2_32.smt2 | unsat (0.446) | unsat (0.565) | unsat (0.408) | unsat (0.416) | unsat (0.398) | unsat (0.411) | unsat (0.404) | unsat (0.358) | unsat (0.400) | unsat (0.533) |
| chc-LIA-Lin_279.smt2_4.smt2 | sat (0.505) | sat (0.564) | sat (0.487) | sat (0.485) | sat (0.466) | sat (0.482) | sat (0.491) | sat (0.484) | unknown (0.658) | sat (0.578) |
| chc-LIA-Lin_279.smt2_5.smt2 | unsat (0.486) | unsat (0.549) | unsat (0.550) | unsat (0.487) | unsat (0.465) | unsat (0.476) | unsat (0.475) | unsat (0.472) | unsat (0.491) | unsat (0.503) |
| chc-LIA-Lin_279.smt2_7.smt2 | unsat (0.443) | unsat (0.531) | unsat (0.410) | unsat (0.395) | unsat (0.425) | unsat (0.394) | unsat (0.412) | unsat (0.393) | unsat (0.408) | unsat (0.418) |
| chc-LIA-Lin_279.smt2_8.smt2 | unsat (0.427) | unsat (0.524) | unsat (0.414) | unsat (0.396) | unsat (0.421) | unsat (0.404) | unsat (0.426) | unsat (0.398) | unsat (0.422) | unsat (0.358) |
| chc-LIA-Lin_279.smt2_9.smt2 | sat (0.426) | sat (0.629) | sat (0.430) | sat (0.396) | sat (0.416) | sat (0.413) | sat (0.408) | sat (0.399) | unknown (0.431) | sat (0.441) |
| chc-LIA-Lin_280.smt2_0.smt2 | sat (0.413) | sat (0.555) | sat (0.455) | sat (0.432) | sat (0.422) | sat (0.414) | sat (0.411) | sat (0.411) | unknown (0.416) | sat (0.426) |
| chc-LIA-Lin_280.smt2_1.smt2 | unsat (0.410) | unsat (0.491) | unsat (0.391) | unsat (0.424) | unsat (0.459) | unsat (0.391) | unsat (0.387) | unsat (0.388) | unsat (0.395) | unsat (0.397) |
| chc-LIA-Lin_280.smt2_10.smt2 | sat (0.428) | sat (0.559) | sat (0.446) | sat (0.401) | sat (0.406) | sat (0.399) | sat (0.412) | sat (0.351) | unknown (0.396) | sat (0.433) |
| chc-LIA-Lin_280.smt2_11.smt2 | unsat (0.433) | unsat (0.523) | unsat (0.425) | unsat (0.389) | unsat (0.355) | unsat (0.407) | unsat (0.404) | unsat (0.382) | unsat (0.385) | unsat (0.411) |
| chc-LIA-Lin_280.smt2_12.smt2 | sat (0.385) | sat (0.556) | sat (0.384) | sat (0.385) | sat (0.402) | sat (0.417) | sat (0.432) | sat (0.417) | unknown (0.409) | sat (0.430) |
| chc-LIA-Lin_280.smt2_13.smt2 | sat (0.437) | sat (0.546) | sat (0.423) | sat (0.411) | sat (0.408) | sat (0.415) | sat (0.414) | sat (0.383) | unknown (0.423) | sat (0.431) |
| chc-LIA-Lin_280.smt2_14.smt2 | unsat (0.408) | unsat (0.533) | unsat (0.405) | unsat (0.384) | unsat (0.412) | unsat (0.405) | unsat (0.413) | unsat (0.373) | unsat (0.419) | unsat (0.385) |
| chc-LIA-Lin_280.smt2_16.smt2 | sat (0.435) | sat (0.553) | sat (0.450) | sat (0.425) | sat (0.419) | sat (0.425) | sat (0.439) | sat (0.431) | unknown (0.424) | sat (0.463) |
| chc-LIA-Lin_280.smt2_17.smt2 | sat (0.454) | sat (0.553) | sat (0.433) | sat (0.419) | sat (0.423) | sat (0.439) | sat (0.443) | sat (0.432) | unknown (0.406) | sat (0.445) |
| chc-LIA-Lin_280.smt2_18.smt2 | unsat (0.534) | unsat (0.807) | unsat (0.640) | unsat (0.544) | unsat (0.509) | unsat (0.524) | unsat (0.541) | unsat (0.523) | unsat (0.513) | unsat (0.460) |
| chc-LIA-Lin_280.smt2_19.smt2 | sat (0.430) | sat (0.577) | sat (0.423) | sat (0.448) | sat (0.430) | sat (0.423) | sat (0.417) | sat (0.410) | unknown (0.426) | sat (0.478) |
| chc-LIA-Lin_280.smt2_2.smt2 | unsat (0.320) | unsat (0.523) | unsat (0.392) | unsat (0.425) | unsat (0.402) | unsat (0.402) | unsat (0.396) | unsat (0.447) | unsat (0.396) | unsat (0.447) |
| chc-LIA-Lin_280.smt2_20.smt2 | unsat (0.418) | unsat (0.540) | unsat (0.386) | unsat (0.429) | unsat (0.406) | unsat (0.397) | unsat (0.389) | unsat (0.389) | unsat (0.389) | unsat (0.439) |
| chc-LIA-Lin_280.smt2_22.smt2 | sat (0.375) | sat (0.625) | sat (0.468) | sat (0.475) | sat (0.452) | sat (0.446) | sat (0.432) | sat (0.444) | unknown (0.414) | sat (0.474) |
| chc-LIA-Lin_280.smt2_23.smt2 | sat (0.362) | sat (0.601) | sat (0.424) | sat (0.410) | sat (0.441) | sat (0.468) | sat (0.441) | sat (0.425) | unknown (0.470) | sat (0.459) |
| chc-LIA-Lin_280.smt2_24.smt2 | unsat (0.551) | unsat (0.560) | unsat (0.403) | unsat (0.625) | unsat (0.641) | unsat (0.570) | unsat (0.544) | unsat (0.521) | unsat (0.594) | unsat (0.472) |
| chc-LIA-Lin_280.smt2_25.smt2 | sat (0.446) | sat (0.553) | sat (0.427) | sat (0.460) | sat (0.496) | sat (0.414) | sat (0.395) | sat (0.427) | unknown (0.409) | sat (0.502) |
| chc-LIA-Lin_280.smt2_26.smt2 | unsat (0.432) | unsat (0.519) | unsat (0.391) | unsat (0.429) | unsat (0.470) | unsat (0.405) | unsat (0.406) | unsat (0.385) | unsat (0.363) | unsat (0.467) |
| chc-LIA-Lin_280.smt2_28.smt2 | sat (0.430) | sat (0.619) | sat (0.422) | sat (0.436) | sat (0.408) | sat (0.409) | sat (0.418) | sat (0.364) | unknown (0.448) | sat (0.456) |
| chc-LIA-Lin_280.smt2_29.smt2 | sat (0.432) | sat (0.609) | sat (0.425) | sat (0.434) | sat (0.423) | sat (0.356) | sat (0.418) | sat (0.392) | unknown (0.418) | sat (0.524) |
| chc-LIA-Lin_280.smt2_3.smt2 | sat (0.403) | sat (0.534) | sat (0.405) | sat (0.464) | sat (0.418) | sat (0.415) | sat (0.344) | sat (0.385) | unknown (0.441) | sat (0.486) |
| chc-LIA-Lin_280.smt2_30.smt2 | unsat (0.401) | unsat (0.585) | unsat (0.390) | unsat (0.439) | unsat (0.406) | unsat (0.377) | unsat (0.400) | unsat (0.399) | unsat (0.425) | unsat (0.507) |
| chc-LIA-Lin_280.smt2_32.smt2 | unsat (0.391) | unsat (0.566) | unsat (0.394) | unsat (0.430) | unsat (0.400) | unsat (0.346) | unsat (0.393) | unsat (0.361) | unsat (0.427) | unsat (0.571) |
| chc-LIA-Lin_280.smt2_5.smt2 | unsat (0.430) | unsat (0.591) | unsat (0.405) | unsat (0.426) | unsat (0.393) | unsat (0.417) | unsat (0.395) | unsat (0.388) | unsat (0.397) | unsat (0.549) |
| chc-LIA-Lin_280.smt2_6.smt2 | sat (0.401) | sat (0.623) | sat (0.438) | sat (0.464) | sat (0.398) | sat (0.402) | sat (0.409) | sat (0.430) | unknown (0.360) | sat (0.594) |
| chc-LIA-Lin_280.smt2_7.smt2 | unsat (0.395) | unsat (0.544) | unsat (0.395) | unsat (0.439) | unsat (0.377) | unsat (0.372) | unsat (0.403) | unsat (0.356) | unsat (0.434) | unsat (0.590) |
| chc-LIA-Lin_280.smt2_8.smt2 | unsat (0.394) | unsat (0.533) | unsat (0.474) | unsat (0.526) | unsat (0.372) | unsat (0.392) | unsat (0.475) | unsat (0.500) | unsat (0.531) | unsat (0.620) |
| chc-LIA-Lin_280.smt2_9.smt2 | sat (0.419) | sat (0.548) | sat (0.497) | sat (0.644) | sat (0.409) | sat (0.391) | sat (0.492) | sat (0.516) | unknown (0.513) | sat (0.550) |
| chc-LIA-Lin_281.smt2_1.smt2 | unsat (0.395) | unsat (0.557) | unsat (0.385) | unsat (0.359) | unsat (0.374) | unsat (0.404) | unsat (0.379) | unsat (0.408) | unsat (0.427) | unsat (0.377) |
| chc-LIA-Lin_281.smt2_10.smt2 | sat (0.383) | sat (0.505) | sat (0.474) | sat (0.513) | sat (0.390) | sat (0.387) | sat (0.472) | sat (0.490) | sat (0.496) | sat (0.577) |
| chc-LIA-Lin_281.smt2_11.smt2 | unsat (0.382) | unsat (0.541) | unsat (0.395) | unsat (0.380) | unsat (0.383) | unsat (0.475) | unsat (0.399) | unsat (0.394) | unsat (0.386) | unsat (0.508) |
| chc-LIA-Lin_281.smt2_12.smt2 | sat (0.492) | sat (0.596) | sat (0.398) | sat (0.565) | sat (0.404) | sat (0.468) | sat (0.399) | sat (0.421) | sat (0.476) | sat (0.538) |
| chc-LIA-Lin_281.smt2_13.smt2 | sat (0.480) | sat (0.541) | sat (0.416) | sat (0.482) | sat (0.410) | sat (0.485) | sat (0.361) | sat (0.433) | sat (0.511) | sat (0.514) |
| chc-LIA-Lin_281.smt2_14.smt2 | unsat (0.469) | unsat (0.525) | unsat (0.335) | unsat (0.407) | unsat (0.392) | unsat (0.429) | unsat (0.397) | unsat (0.402) | unsat (0.430) | unsat (0.417) |
| chc-LIA-Lin_281.smt2_16.smt2 | sat (0.489) | sat (0.555) | sat (0.404) | sat (0.404) | sat (0.337) | sat (0.413) | sat (0.410) | sat (0.403) | sat (0.450) | sat (0.460) |
| chc-LIA-Lin_281.smt2_18.smt2 | unsat (0.380) | unsat (0.482) | unsat (0.414) | unsat (0.430) | unsat (0.380) | unsat (0.406) | unsat (0.419) | unsat (0.357) | unsat (0.532) | unsat (0.488) |
| chc-LIA-Lin_281.smt2_19.smt2 | sat (0.406) | sat (0.582) | sat (0.404) | sat (0.429) | sat (0.394) | sat (0.404) | sat (0.416) | sat (0.393) | sat (0.424) | sat (0.438) |
| chc-LIA-Lin_281.smt2_2.smt2 | unsat (0.394) | unsat (0.506) | unsat (0.382) | unsat (0.403) | unsat (0.378) | unsat (0.376) | unsat (0.406) | unsat (0.385) | unsat (0.385) | unsat (0.436) |
| chc-LIA-Lin_281.smt2_20.smt2 | unsat (0.402) | unsat (0.534) | unsat (0.404) | unsat (0.394) | unsat (0.380) | unsat (0.401) | unsat (0.398) | unsat (0.425) | unsat (0.433) | unsat (0.552) |
| chc-LIA-Lin_281.smt2_21.smt2 | sat (0.406) | sat (0.551) | sat (0.408) | sat (0.471) | sat (0.383) | sat (0.390) | sat (0.411) | sat (0.430) | sat (0.406) | sat (3.786) |
| chc-LIA-Lin_281.smt2_22.smt2 | sat (0.407) | sat (0.569) | sat (0.406) | sat (0.336) | sat (0.399) | sat (0.360) | sat (0.405) | sat (0.426) | sat (0.412) | sat (0.484) |
| chc-LIA-Lin_281.smt2_23.smt2 | unsat (0.443) | unsat (0.494) | unsat (0.405) | unsat (0.417) | unsat (0.408) | unsat (0.413) | unsat (0.420) | unsat (0.362) | unsat (0.424) | unsat (0.569) |
| chc-LIA-Lin_281.smt2_24.smt2 | sat (0.416) | sat (0.597) | sat (0.416) | sat (0.427) | sat (0.392) | sat (0.413) | sat (0.393) | sat (0.403) | sat (0.395) | sat (0.442) |
| chc-LIA-Lin_281.smt2_25.smt2 | unsat (0.419) | unsat (0.590) | unsat (0.392) | unsat (0.405) | unsat (0.385) | unsat (0.409) | unsat (0.379) | unsat (0.390) | unsat (0.414) | unsat (0.426) |
| chc-LIA-Lin_281.smt2_28.smt2 | unsat (0.373) | unsat (0.507) | unsat (0.393) | unsat (0.372) | unsat (0.374) | unsat (0.393) | unsat (0.396) | unsat (0.374) | unsat (0.377) | unsat (0.404) |
| chc-LIA-Lin_281.smt2_3.smt2 | sat (0.408) | sat (0.541) | sat (0.383) | sat (0.389) | sat (0.399) | sat (0.370) | sat (0.397) | sat (0.380) | sat (0.389) | sat (0.403) |
| chc-LIA-Lin_281.smt2_30.smt2 | sat (0.400) | sat (0.510) | sat (0.382) | sat (0.383) | sat (0.403) | sat (0.390) | sat (0.391) | sat (0.380) | sat (0.384) | sat (0.402) |
| chc-LIA-Lin_281.smt2_31.smt2 | unsat (0.402) | unsat (0.463) | unsat (0.377) | unsat (0.364) | unsat (0.471) | unsat (0.382) | unsat (0.386) | unsat (0.364) | unsat (0.382) | unsat (0.379) |
| chc-LIA-Lin_281.smt2_32.smt2 | sat (0.416) | sat (0.586) | sat (0.378) | sat (0.393) | sat (0.437) | sat (0.390) | sat (0.382) | sat (0.386) | sat (0.374) | sat (0.388) |
| chc-LIA-Lin_281.smt2_33.smt2 | sat (0.411) | sat (0.577) | sat (0.395) | sat (0.396) | sat (0.475) | sat (0.365) | sat (0.380) | sat (0.370) | sat (0.382) | sat (0.402) |
| chc-LIA-Lin_281.smt2_4.smt2 | sat (0.369) | sat (0.554) | sat (0.407) | sat (0.387) | sat (0.405) | sat (0.386) | sat (0.397) | sat (0.382) | sat (0.383) | sat (0.408) |
| chc-LIA-Lin_281.smt2_5.smt2 | unsat (0.357) | unsat (0.519) | unsat (0.396) | unsat (0.369) | unsat (0.375) | unsat (0.362) | unsat (0.380) | unsat (0.359) | unsat (0.364) | unsat (0.385) |
| chc-LIA-Lin_281.smt2_7.smt2 | unsat (0.360) | unsat (0.467) | unsat (0.373) | unsat (0.369) | unsat (0.406) | unsat (0.382) | unsat (0.377) | unsat (0.377) | unsat (0.362) | unsat (0.392) |
| chc-LIA-Lin_281.smt2_8.smt2 | unsat (0.364) | unsat (0.568) | unsat (0.375) | unsat (0.370) | unsat (0.385) | unsat (0.366) | unsat (0.379) | unsat (0.358) | unsat (0.370) | unsat (0.392) |
| chc-LIA-Lin_281.smt2_9.smt2 | sat (0.370) | sat (0.593) | sat (0.391) | sat (0.388) | sat (0.379) | sat (0.365) | sat (0.382) | sat (0.362) | sat (0.381) | sat (0.438) |