fromJust package:sbv

Return the value of an optional value. The behavior is undefined if passed Nothing, i.e., it can return any value. Compare to fromMaybe.

>>> fromJust (sJust (literal 'a'))
'a' :: SChar

>>> prove $ \x -> fromJust (sJust x) .== (x :: SChar)
Q.E.D.

>>> sat $ \x -> x .== (fromJust sNothing :: SChar)
Satisfiable. Model:
s0 = 'A' :: Char

Note how we get a satisfying assignment in the last case: The behavior is unspecified, thus the SMT solver picks whatever satisfies the constraints, if there is one.