Skip to content

Commit e9f06ae

Browse files
committed
merge Deajun's change
1 parent 0aee5a8 commit e9f06ae

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

src/verification/int_list.k

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,9 @@ module INT-LIST
3737
//rule sorted(L1 @ L2)
3838
// => intseq2intset(L1) <=IntSet intseq2intset(L2) andBool sorted(L1) andBool sorted(L2)
3939
// [smt-lemma]
40+
/* TODO(Daejun): moved into include/z3/sorted_list.smt2 due to translation bug
4041
rule sorted(ListItem(I)) => true [smt-lemma]
4142
rule sorted(.List) => true [smt-lemma]
43+
*/
4244
endmodule
4345

0 commit comments

Comments
 (0)