Method get

src/api/java/Statistics.java:177–187

The value of a particular statistical counter. Remarks: Returns null if the key is unknown. @throws Z3Exception

(String key)

     * @throws Z3Exception
     **/
    public Entry get(String key)
    {
        int n = size();
        Entry[] es = getEntries();
        for (int i = 0; i < n; i++) {
            if (es[i].Key.equals(key)) {
                return es[i];
            }
        }
        return null;
    }

    Statistics(Context ctx, long obj)
    {