kdrag.utils.proofstep_to_smt2

kdrag.utils.proofstep_to_smt2(pf: Proof) → str

Turn a Proof into an smt2 string that should result in unsat >>> x = smt.Int(“x”) >>> p1 = kd.axiom(x > 0) >>> _ = proofstep_to_smt2(kd.prove(x > -1, by=[p1]))

Parameters:

pf (Proof)

Return type:

str