From a062478553c55c7b84922fae2ec7927d298f8a33 Mon Sep 17 00:00:00 2001 From: Ioannis Filippidis Date: Sat, 17 Oct 2020 00:38:45 +0300 Subject: [PATCH] BUG: define UFNIA as logic with integer arithmetic The keyword argument `integer_arithmetic=True` was missing from the constructor of `pysmt.logics.Logic` for the logic UFNIA [1, 2] ("Non-linear integer arithmetic with uninterpreted sort and function symbols." [1]). See for example how the logic QF_UFNIA is defined in the same module. A consequence of the previous definition of UFNIA was type checking errors due to numerals without `'.'` being parsed as reals instead of integers in the module `pysmt.smtlib.parser.parser` [3]. [1] http://smtlib.cs.uiowa.edu/logics.shtml [2] http://smtlib.cs.uiowa.edu/logics-all.shtml#UFNIA [3] https://github.com/pysmt/pysmt/blob/35ac3fd88b01706ba01d2a7cf291194fda0c8f92/pysmt/smtlib/parser/parser.py#L665-L672 --- pysmt/logics.py | 1 + 1 file changed, 1 insertion(+) diff --git a/pysmt/logics.py b/pysmt/logics.py index dfdeb2434..5c76f402c 100644 --- a/pysmt/logics.py +++ b/pysmt/logics.py @@ -590,6 +590,7 @@ def __hash__(self): description=\ """Non-linear integer arithmetic with uninterpreted sort and function symbols.""", + integer_arithmetic=True, integer_difference=True, linear=False, uninterpreted=True)