mirror of
https://github.com/Z3Prover/z3
synced 2025-04-13 12:28:44 +00:00
fix build break regarind z3test.py and added rlimit
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
f3b8fe130a
commit
1f9d5249a3
|
@ -5640,7 +5640,7 @@ class Statistics:
|
|||
sat
|
||||
>>> st = s.statistics()
|
||||
>>> len(st)
|
||||
5
|
||||
6
|
||||
"""
|
||||
return int(Z3_stats_size(self.ctx.ref(), self.stats))
|
||||
|
||||
|
@ -5654,7 +5654,7 @@ class Statistics:
|
|||
sat
|
||||
>>> st = s.statistics()
|
||||
>>> len(st)
|
||||
5
|
||||
6
|
||||
>>> st[0]
|
||||
('nlsat propagations', 2)
|
||||
>>> st[1]
|
||||
|
@ -5678,7 +5678,7 @@ class Statistics:
|
|||
sat
|
||||
>>> st = s.statistics()
|
||||
>>> st.keys()
|
||||
['nlsat propagations', 'nlsat stages', 'max memory', 'memory', 'num allocs']
|
||||
['nlsat propagations', 'nlsat stages', 'rlimit count', 'max memory', 'memory', 'num allocs']
|
||||
"""
|
||||
return [Z3_stats_get_key(self.ctx.ref(), self.stats, idx) for idx in range(len(self))]
|
||||
|
||||
|
@ -5715,7 +5715,7 @@ class Statistics:
|
|||
sat
|
||||
>>> st = s.statistics()
|
||||
>>> st.keys()
|
||||
['nlsat propagations', 'nlsat stages', 'max memory', 'memory', 'num allocs']
|
||||
['nlsat propagations', 'nlsat stages', 'rlimit count', 'max memory', 'memory', 'num allocs']
|
||||
>>> st.nlsat_propagations
|
||||
2
|
||||
>>> st.nlsat_stages
|
||||
|
|
|
@ -238,5 +238,5 @@ void get_memory_statistics(statistics& st) {
|
|||
}
|
||||
|
||||
void get_rlimit_statistics(reslimit& l, statistics& st) {
|
||||
st.update("rlimit-count", l.count());
|
||||
st.update("rlimit count", l.count());
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue