Skip to content

Instantly share code, notes, and snippets.

/gist:ce7b96acf712ac16299e

Created June 11, 2015 13:07
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save anonymous/ce7b96acf712ac16299e to your computer and use it in GitHub Desktop.
Save anonymous/ce7b96acf712ac16299e to your computer and use it in GitHub Desktop.
Download ZIP
Z3 statistics (4.4.0)
Raw
gistfile1.txt
(:version "4.4.0")
(:add-rows 199940
:added-eqs 1593465
:arith-conflicts 687
:assert-diseq 23469
:assert-lower 208896
:assert-upper 207038
:bound-prop 9623
:conflicts 2779
:datatype-accessor-ax 19
:datatype-constructor-ax 630
:datatype-occurs-check 29412
:datatype-splits 630
:decisions 215165
:del-clause 2796292
:eq-adapter 166208
:final-checks 496
:fixed-eqs 132157
:interface-eqs 270
:max-generation 30
:memory 17.44
:minimized-lits 1461
:mk-clause 2803473
:num-checks 188
:offset-eqs 143053
:pivots 40545
:propagations 1313562
:quant-instantiations 643860
:restarts 6
:time 4.52)
success
[quantifier_instances] k!796 : 474 : 2 : 3
[quantifier_instances] k!796 : 1029 : 2 : 3
[quantifier_instances] k!796 : 474 : 2 : 3
[quantifier_instances] k!796 : 1029 : 2 : 3
[quantifier_instances] k!17703 : 299 : 6 : 7
[quantifier_instances] k!12520 : 428 : 6 : 7
[quantifier_instances] k!17599 : 366 : 6 : 7
[quantifier_instances] k!17010 : 119 : 4 : 5
[quantifier_instances] k!16980 : 339 : 4 : 5
[quantifier_instances] k!16906 : 291 : 6 : 7
[quantifier_instances] k!796 : 966 : 2 : 3
[quantifier_instances] k!11917 : 75 : 5 : 6
[quantifier_instances] k!11899 : 97 : 5 : 5
[quantifier_instances] k!11740 : 674 : 5 : 6
[quantifier_instances] k!796 : 1036 : 2 : 3
[quantifier_instances] k!796 : 1554 : 3 : 4
[quantifier_instances] k!796 : 8938 : 4 : 5
[quantifier_instances] k!796 : 1210 : 2 : 3
[quantifier_instances] k!11656 : 476 : 8 : 9
[quantifier_instances] k!11638 : 855 : 8 : 9
[quantifier_instances] k!11598 : 709 : 8 : 8
[quantifier_instances] k!10729 : 680 : 5 : 6
[quantifier_instances] k!10722 : 1 : 5 : 6
[quantifier_instances] k!796 : 1086 : 2 : 3
[quantifier_instances] k!796 : 1629 : 3 : 4
[quantifier_instances] k!796 : 9189 : 4 : 5
[quantifier_instances] k!796 : 1162 : 2 : 3
[quantifier_instances] k!10645 : 610 : 9 : 10
[quantifier_instances] k!10627 : 839 : 9 : 10
[quantifier_instances] k!10587 : 672 : 9 : 9
[quantifier_instances] k!9718 : 674 : 5 : 6
[quantifier_instances] k!796 : 1127 : 2 : 3
[quantifier_instances] k!796 : 1686 : 3 : 4
[quantifier_instances] k!796 : 9401 : 4 : 5
[quantifier_instances] k!232 : 10760 : 29 : 30 // x in xs[..n] <==> ... (first inner exists 2)
[quantifier_instances] k!188 : 2 : 5 : 6
[quantifier_instances] k!256 : 10760 : 29 : 30 // x in xs[n..] <==> ... (first inner exists 3)
[quantifier_instances] k!188 : 647 : 5 : 6
[quantifier_instances] k!796 : 4862 : 4 : 5
[quantifier_instances] k!796 : 1378 : 2 : 3
[quantifier_instances] k!796 : 4114 : 4 : 5
[quantifier_instances] k!796 : 2111 : 3 : 4
[quantifier_instances] k!796 : 12730 : 4 : 5
[quantifier_instances] k!796 : 1844 : 2 : 3
[quantifier_instances] k!2996 : 1604 : 29 : 30
[quantifier_instances] k!2990 : 15759 : 29 : 30
[quantifier_instances] k!796 : 1667 : 2 : 3
[quantifier_instances] k!796 : 1859 : 2 : 3
[quantifier_instances] k!796 : 1667 : 2 : 3
[quantifier_instances] k!796 : 1859 : 2 : 3
[quantifier_instances] k!2283 : 10145 : 29 : 30
[quantifier_instances] k!2814 : 6494 : 29 : 30
[quantifier_instances] k!2421 : 1733 : 28 : 29
[quantifier_instances] k!2411 : 10898 : 28 : 29
[quantifier_instances] k!796 : 13057 : 5 : 6
[quantifier_instances] k!2164 : 1 : 2 : 3
[quantifier_instances] k!2154 : 15059 : 29 : 30
[quantifier_instances] k!2149 : 155 : 24 : 25
[quantifier_instances] k!796 : 13057 : 5 : 6
[quantifier_instances] k!2127 : 1350 : 28 : 29
[quantifier_instances] k!2117 : 15059 : 29 : 30
[quantifier_instances] k!2112 : 318 : 24 : 25
[quantifier_instances] k!796 : 13057 : 5 : 6
[quantifier_instances] k!2087 : 100 : 29 : 30
[quantifier_instances] k!2082 : 11000 : 29 : 30
[quantifier_instances] k!2077 : 15058 : 29 : 30
[quantifier_instances] k!2072 : 217 : 24 : 25
[quantifier_instances] k!1989 : 1643 : 29 : 30
[quantifier_instances] k!1984 : 15874 : 29 : 30
[quantifier_instances] k!1499 : 1 : 2 : 3
[quantifier_instances] k!1489 : 15082 : 29 : 30
[quantifier_instances] k!1484 : 154 : 24 : 25
[quantifier_instances] k!1466 : 8153 : 28 : 29
[quantifier_instances] k!1456 : 15082 : 29 : 30
[quantifier_instances] k!1451 : 152 : 24 : 25
[quantifier_instances] k!1430 : 6617 : 29 : 30
[quantifier_instances] k!1425 : 8694 : 29 : 30
[quantifier_instances] k!1420 : 15082 : 29 : 30
[quantifier_instances] k!1415 : 152 : 24 : 25
[quantifier_instances] k!188 : 8684 : 29 : 30 // x in xs <==> ... (first inner exists 1)
[quantifier_instances] k!1358 : 4 : 0 : 1
[quantifier_instances] k!1352 : 4 : 0 : 1
[quantifier_instances] k!1320 : 2 : 0 : 1
[quantifier_instances] k!1295 : 2 : 0 : 1
[quantifier_instances] k!1282 : 132 : 0 : 1
[quantifier_instances] k!1270 : 158 : 2 : 3
[quantifier_instances] k!1258 : 270 : 3 : 3
[quantifier_instances] k!1246 : 12 : 0 : 1
[quantifier_instances] k!804 : 54 : 3 : 4
[quantifier_instances] k!798 : 41338 : 3 : 4
[quantifier_instances] k!731 : 41 : 1 : 2
[quantifier_instances] k!717 : 5764 : 8 : 9
[quantifier_instances] k!711 : 3304 : 5 : 6
[quantifier_instances] k!705 : 100351 : 4 : 5
[quantifier_instances] k!663 : 81290 : 5 : 6
[quantifier_instances] k!631 : 4296 : 29 : 30
[quantifier_instances] k!622 : 1353 : 8 : 9
[quantifier_instances] k!617 : 749 : 5 : 6
[quantifier_instances] k!437 : 3490 : 29 : 30
[quantifier_instances] k!381 : 148 : 3 : 4
[quantifier_instances] k!377 : 479 : 3 : 4
[quantifier_instances] k!373 : 4 : 2 : 3
[quantifier_instances] k!358 : 336 : 8 : 9
[quantifier_instances] k!327 : 762 : 5 : 6
[quantifier_instances] k!321 : 162 : 4 : 5
[quantifier_instances] k!316 : 901 : 7 : 8
[quantifier_instances] k!310 : 277 : 3 : 4
[quantifier_instances] k!290 : 18 : 0 : 1
[quantifier_instances] k!287 : 18 : 0 : 1
[quantifier_instances] k!268 : 1061 : 8 : 9 // x in xs[n..] <==> ... (outer forall 3)
[quantifier_instances] k!244 : 804 : 3 : 4 // x in xs[..n] <==> ... (outer forall 2)
[quantifier_instances] k!211 : 454 : 1 : 2
[quantifier_instances] k!199 : 1755 : 8 : 9 // x in xs <==> ... (outer forall 1)
[quantifier_instances] k!165 : 2013 : 5 : 6
[quantifier_instances] k!160 : 179 : 7 : 8
[quantifier_instances] k!157 : 3 : 2 : 3
[quantifier_instances] k!143 : 12 : 4 : 5
[quantifier_instances] k!139 : 18 : 4 : 5
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment