Is there a way to pass assumptions from (check-sat ...) statement of SMT2 formula into the solver ?
Consider the following example formula stored in ex.smt2:
# cat ex.smt2
(declare-fun p () Bool)
(assert (not p))
(check-sat p)
Running z3 on it gives unsat, as expected. Now, I'd like to solve with assumptions (p) through z3py interface:
In [30]: ctx = z3.Context()
In [31]: s = z3.Solver(ctx=ctx)
In [32]: f = z3.parse_smt2_file("ex.smt2", ctx=ctx)
In [33]: s.add(f)
In [34]: s.check()
Out[34]: sat
Is there an API to get assumptions (i.e. (p) in this example) from the parser ? Or even better, just tell the solver to solve with the assumptions read from the input file ?
