From 9e8e12a5ba12153d931c8cf119cdd39e1702b946 Mon Sep 17 00:00:00 2001 From: Luca Di Stefano Date: Thu, 18 Dec 2025 10:20:14 +0100 Subject: [PATCH] ltlmt: skip sat check for assumptions w/ ltl --- src/parsing/string_to_ltlmt.py | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/parsing/string_to_ltlmt.py b/src/parsing/string_to_ltlmt.py index cf3480e8..e433262b 100644 --- a/src/parsing/string_to_ltlmt.py +++ b/src/parsing/string_to_ltlmt.py @@ -354,7 +354,11 @@ def ltlmt2prog(self, formulas, name="fromTSL"): init_values = [(str(x), types[str(x)], init_type_values(x)) for x in self.vars] # TODO use this init_assumptions to limit env init transitions - if not sat(conjunct_formula_set(init_assumptions), types): + try: + satisfiable_assumptions = sat(conjunct_formula_set(init_assumptions), types) + except NotImplementedError: + satisfiable_assumptions = True + if not satisfiable_assumptions: raise Exception( "Unsatisfiable initial assumptions: " + "\n".join(map(str, init_assumptions))