You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Currently, the translation of the binary rule @split is hard coded to produce one of the two possible results. It has to be fixed such that the result to be produced is inferred from the arguments that are present in the SMTInterpol proof.
Fix @split (case detection, massaging to make it work with SMTCoq formulas)
Add another test proof that tests the symetric split case
The text was updated successfully, but these errors were encountered:
Currently, the translation of the binary rule @split is hard coded to produce one of the two possible results. It has to be fixed such that the result to be produced is inferred from the arguments that are present in the SMTInterpol proof.
The text was updated successfully, but these errors were encountered: