diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-01-20 07:28:29 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-01-20 09:28:29 -0600 |
commit | e2ec4e5401eba4ef63539ddb7c1f3a54301de4b1 (patch) | |
tree | d17d5a42599eec5699d646e2ffe3150771ff7aff /test/regress/regress1 | |
parent | c8e8acd26b4bd5c47110b9448a74a45913b5518f (diff) |
SMT2 parser: Do not add non-linear symbols for linear Int arith logics. (#5787)
This enables more strict handling of operators div, mod and abs
for Integer arithmetic logics.
More strict handling for '/' for Real arithmetic logics is more involved
and should be done in the parser -- instead at solving time, like is
currently done for checking that the application * is in the linear
fragment. The latter should be checked in the parser, too.
This is postponed to a later PR.
Diffstat (limited to 'test/regress/regress1')
5 files changed, 7 insertions, 5 deletions
diff --git a/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt2 b/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt2 index dd9cb6886..efcae64bc 100644 --- a/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt2 +++ b/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --fmf-fun --no-check-models ; EXPECT: sat -(set-logic UFLIA) +(set-logic UFNIA) (set-info :status sat) (define-fun-rec int-and ((n Int) (n1 Int) (n2 Int)) Bool ( or diff --git a/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2 b/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2 index ea5a5e4b7..32e9d4178 100644 --- a/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2 +++ b/test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --fmf-fun --no-check-models ; EXPECT: sat -(set-logic UFLIA) +(set-logic UFNIA) (set-info :status sat) (define-fun-rec int-and ((n Int) (n1 Int) (n2 Int)) Bool ( or diff --git a/test/regress/regress1/quantifiers/issue5484-qe.smt2 b/test/regress/regress1/quantifiers/issue5484-qe.smt2 index c2499ed16..9fcc7dcba 100644 --- a/test/regress/regress1/quantifiers/issue5484-qe.smt2 +++ b/test/regress/regress1/quantifiers/issue5484-qe.smt2 @@ -1,7 +1,8 @@ +; COMMAND-LINE: -q ; SCRUBBER: sed 's/(.*)/()/g' ; EXPECT: () ; EXIT: 0 -(set-logic LIA) +(set-logic NIA) (declare-fun v9 () Bool) (declare-fun v18 () Bool) (declare-fun i2 () Int) diff --git a/test/regress/regress1/quantifiers/issue5484b-qe.smt2 b/test/regress/regress1/quantifiers/issue5484b-qe.smt2 index 86f999504..754603135 100644 --- a/test/regress/regress1/quantifiers/issue5484b-qe.smt2 +++ b/test/regress/regress1/quantifiers/issue5484b-qe.smt2 @@ -1,7 +1,8 @@ +; COMMAND-LINE: -q ; SCRUBBER: sed 's/(.*)/()/g' ; EXPECT: () ; EXIT: 0 -(set-logic LIA) +(set-logic NIA) (declare-fun v0 () Bool) (declare-fun v1 () Bool) (declare-fun v2 () Bool) diff --git a/test/regress/regress1/quantifiers/lia-witness-div-pp.smt2 b/test/regress/regress1/quantifiers/lia-witness-div-pp.smt2 index bd42e3596..62babf518 100644 --- a/test/regress/regress1/quantifiers/lia-witness-div-pp.smt2 +++ b/test/regress/regress1/quantifiers/lia-witness-div-pp.smt2 @@ -1,5 +1,5 @@ (set-info :smt-lib-version 2.6) -(set-logic LIA) +(set-logic NIA) (set-info :status unsat) (declare-fun c_main_~x~0 () Int) (declare-fun c_main_~y~0 () Int) |