unicode_fol_kit.is_satisfiable¶ unicode_fol_kit.is_satisfiable(formula, timeout=10000)[source]¶ Return True if the formula has a model (Z3 reports sat). A Z3 unknown result (e.g. on hard quantified formulas hitting the timeout) is treated as not-known-satisfiable and returns False. Parameters: formula (Node) timeout (int) Return type: bool