| Name: |
interface-with-overflows-k5-liveness.aag |
| md5: |
0c7ea8a2edad4407054af3b375b91eb6 |
| FractionOfBinaryClauses |
None |
| FractionOfNegativeLiteralsPerClauseEntropy |
None |
| FractionOfNegativeLiteralsPerClauseMax |
None |
| FractionOfNegativeLiteralsPerClauseMean |
None |
| FractionOfNegativeLiteralsPerClauseMin |
None |
| FractionOfNegativeLiteralsPerClauseVariationCoefficient |
None |
| FractionOfNegativeVariablesEntropy |
None |
| FractionOfNegativeVariablesMax |
None |
| FractionOfNegativeVariablesMean |
None |
| FractionOfNegativeVariablesMin |
None |
| FractionOfNegativeVariablesVariationCoefficient |
None |
| FractionOfPositiveLiteralsPerClauseEntropy |
None |
| FractionOfPositiveLiteralsPerClauseMax |
None |
| FractionOfPositiveLiteralsPerClauseMean |
None |
| FractionOfPositiveLiteralsPerClauseMin |
None |
| FractionOfPositiveLiteralsPerClauseVariationCoefficient |
None |
| FractionOfPositiveVariablesEntropy |
None |
| FractionOfPositiveVariablesMax |
None |
| FractionOfPositiveVariablesMean |
None |
| FractionOfPositiveVariablesMin |
None |
| FractionOfPositiveVariablesVariationCoefficient |
None |
| FractionOfTernaryClauses |
None |
| FractionOfUnaryClauses |
None |
| ClausesToVariablesRatio |
None |
| ClausesToVariablesRatioCubic |
None |
| ClausesToVariablesRatioQuadratic |
None |
| LinearizedClausesToVariablesRatio |
None |
| LinearizedClausesToVariablesRatioQuadratic |
None |
| LinearizedClaustesToVariablesRatioCubic |
None |
| NumberOfClauses |
None |
| NumberOfVariables |
None |
| VariablesToClausesRatio |
None |
| VariablesToClausesRatioCubic |
None |
| VariablesToClausesRatioQuadratic |
None |
| ClauseNodeDegreesEntropy |
None |
| ClauseNodeDegreesMax |
None |
| ClauseNodeDegreesMean |
None |
| ClauseNodeDegreesMin |
None |
| ClauseNodeDegreesVariationCoefficient |
None |
| VariableNodeDegreesEntropy |
None |
| VariableNodeDegreesMax |
None |
| VariableNodeDegreesMean |
None |
| VariableNodeDegreesMin |
None |
| VariableNodeDegreesVariationCoefficient |
None |
| DegreeEntropy |
None |
| DegreeMax |
None |
| DegreeMean |
None |
| DegreeMin |
None |
| DegreeVariationCoefficient |
None |
aag 1958 7 50 1 1901
2
4
6
8
10
12
14
16 958
18 962
20 966
22 970
24 974
26 978
28 982
30 986
32 990
34 13
36 1014
38 1020
40 1026
42 1032
44 1038
46 1054
48 1062
50 1070
52 1078
54 1086
56 1092
58 1098
60 1104
62 1110
64 1116
66 1132
68 1186
70 1236
72 1310
74 1378
76 1395
78 2284
80 2670
82 2950
84 3168
86 3406
88 3630
90 3671
92 3694
94 3718
96 3735
98 3736
100 3795
102 3832
104 3837
106 3846
108 3852
110 3854
112 3859
114 3901
3917
116 34 33
118 116 31
120 118 28
122 120 27
124 122 25
126 124 23
128 126
... [truncated 25.9 kB]
2.state@0
l37 sys_prop_spec8.state@2
l38 sys_prop_spec8.state@1
l39 sys_prop_spec8.state@0
l40 sys_prop_spec4.state@1
l41 sys_prop_spec4.state@0
l42 sys_prop_spec1.state@1
l43 sys_prop_spec1.state@0
l44 sys_prop_counting_fairness.state
l45 counter_latch
l46 counter_latch
l47 counter_latch
l48 counter_latch
l49 AIGMOVE_INVALID_LATCH
o0 AIGER_OR
c
aigor
disjunction of 2 original outputs
#!SYNTCOMP
STATUS : unrealizable
SOLVED_BY : 3/3 [2015-pre-classification]
SOLVED_IN : 2.52992 [2015-pre-classification]
#.