From 195ba0a9a49bb658c50aabd148f59e553967b6cb Mon Sep 17 00:00:00 2001 From: ntsis Date: Thu, 9 Nov 2023 11:55:12 -0800 Subject: [PATCH] add/remove extra lines --- include/sort_inference.h | 3 --- tests/smt2/qf_s/test-ops-SLIA.smt2 | 2 +- tests/smt2/qf_s/test-ops.smt2 | 2 +- 3 files changed, 2 insertions(+), 5 deletions(-) diff --git a/include/sort_inference.h b/include/sort_inference.h index 40b43a547..aa3efbb99 100644 --- a/include/sort_inference.h +++ b/include/sort_inference.h @@ -168,7 +168,6 @@ bool check_store_sorts(const SortVec & sorts); * @param returns true iff the first sort is the string sort * and the next two match the int sort */ - bool check_substr_sorts(const SortVec & sorts); /** Checks if the sorts are well-sorted for a char at operator @@ -176,7 +175,6 @@ bool check_substr_sorts(const SortVec & sorts); * @param returns true iff the first sort is the string sort * and the second is the int sort */ - bool check_charat_sorts(const SortVec & sorts); /** Checks if the sorts are well-sorted for an index of operator @@ -184,7 +182,6 @@ bool check_charat_sorts(const SortVec & sorts); * @param returns true iff the first two sorts are the string sort * and the third is the int sort */ - bool check_indexof_sorts(const SortVec & sorts); bool bool_sorts(const SortVec & sorts); diff --git a/tests/smt2/qf_s/test-ops-SLIA.smt2 b/tests/smt2/qf_s/test-ops-SLIA.smt2 index a07ff2e16..fe7da3c58 100644 --- a/tests/smt2/qf_s/test-ops-SLIA.smt2 +++ b/tests/smt2/qf_s/test-ops-SLIA.smt2 @@ -72,4 +72,4 @@ (assert (not (str.is_digit "A"))) (assert (not (str.is_digit "10"))) -(check-sat) \ No newline at end of file +(check-sat) diff --git a/tests/smt2/qf_s/test-ops.smt2 b/tests/smt2/qf_s/test-ops.smt2 index 7f2a8092a..b8b0ad7dd 100644 --- a/tests/smt2/qf_s/test-ops.smt2 +++ b/tests/smt2/qf_s/test-ops.smt2 @@ -60,4 +60,4 @@ (assert (not (str.is_digit "A"))) (assert (not (str.is_digit "10"))) -(check-sat) \ No newline at end of file +(check-sat)