From e2dc7c6f64e66b1ce8c1c53980833ede5cf2828d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 12 Feb 2016 17:12:43 +0000
Subject: [PATCH] add note that current re.complement is non-standard

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/seq_rewriter.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index c9745a46b..af0fc6b74 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -125,6 +125,7 @@ eautomaton* re2automaton::re2aut(expr* e) {
         }
     }
     else if (u.re.is_complement(e, e0)) {
+        // TBD non-standard semantics of complementation.
         if (u.re.is_range(e0, e1, e2) && u.str.is_string(e1, s1) && u.str.is_string(e2, s2) &&
             s1.length() == 1 && s2.length() == 1) {
             unsigned start = s1[0];