Skip to content

Commit

Permalink
add/remove extra lines
Browse files Browse the repository at this point in the history
  • Loading branch information
ntsis committed Nov 9, 2023
1 parent 23e792a commit 195ba0a
Show file tree
Hide file tree
Showing 3 changed files with 2 additions and 5 deletions.
3 changes: 0 additions & 3 deletions include/sort_inference.h
Original file line number Diff line number Diff line change
Expand Up @@ -168,23 +168,20 @@ 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
* @param sorts the vector of 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
* @param sorts the vector of 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);
Expand Down
2 changes: 1 addition & 1 deletion tests/smt2/qf_s/test-ops-SLIA.smt2
Original file line number Diff line number Diff line change
Expand Up @@ -72,4 +72,4 @@
(assert (not (str.is_digit "A")))
(assert (not (str.is_digit "10")))

(check-sat)
(check-sat)
2 changes: 1 addition & 1 deletion tests/smt2/qf_s/test-ops.smt2
Original file line number Diff line number Diff line change
Expand Up @@ -60,4 +60,4 @@
(assert (not (str.is_digit "A")))
(assert (not (str.is_digit "10")))

(check-sat)
(check-sat)

0 comments on commit 195ba0a

Please sign in to comment.