def z3_implies_batch(premise, formulas, timeout=False):
    #import IPython
    #IPython.embed()
    s = z3.Solver()
    if timeout:
        s.set("timeout", 2000) # 2 seconds
        #s.set("timeout", 60000) # 1 minute
    s.add(to_z3(premise))
    result = []
    for f in formulas:
        key = (premise, f)
        if key in _implies_cache:
            result.append(_implies_cache[key])
        else:
            s.push()
            s.add(to_z3(Not(f)))
            res = s.check()
            s.pop()
            if res == z3.sat:
                _implies_cache[key] = False
                result.append(False)
            elif res == z3.unsat:
                _implies_cache[key] = True
                result.append(True)
            else:
                # no caching of unknown results
                print "z3 returned: {}".format(res)
                assert False
                result.append(None)
    return result
Use z3 to test if premise implies each formula in formulas
dataset/ETHPy150Open Microsoft/ivy/ivy/z3_utils.py/z3_implies_batch