Repository: pysmt/pysmt (python)

Issue:
`SmtLibParser` fails to parse annotations without associated values
When parsing annotations, the parser always tries to read an associated value:
https://github.com/pysmt/pysmt/blob/8aaf1d3309e7402db20fafd6075a9ce7142fed85/pysmt/smtlib/parser/parser.py#L773-L790

However, following the SMT-LIB specs:
```
〈attribute_value〉 ::= 〈spec_constant〉 | 〈symbol〉 | ( 〈s_expr〉∗ )
〈attribute〉 ::= 〈keyword〉 | 〈keyword〉 〈attribute_value〉
```
An attribute can also be a single keyword, without any associated value.

Pull request description:
Parse value annotations with ":" as keywords
Fixes #809 


Patch:
diff --git a/pysmt/smtlib/parser/parser.py b/pysmt/smtlib/parser/parser.py
index 40f5ec5..2a14fa9 100644
--- a/pysmt/smtlib/parser/parser.py
+++ b/pysmt/smtlib/parser/parser.py
@@ -773,6 +773,11 @@ class SmtLibParser(object):
             keyword = tk[1:]
             tk = tokens.consume()
             value = None
+            if tk.startswith(":") or tk == ")":
+                # another annotation keyword instead of a value of the previous annotation
+                # add previous annotation with None value and continue to next iteration
+                self.cache.annotations.add(term, keyword, value)
+                continue
             if tk == "(":
                 counter = 1
                 buff = [tk]


Test patch:
diff --git a/pysmt/test/smtlib/test_annotations.py b/pysmt/test/smtlib/test_annotations.py
index bcda7af..8e0b764 100644
--- a/pysmt/test/smtlib/test_annotations.py
+++ b/pysmt/test/smtlib/test_annotations.py
@@ -167,8 +167,10 @@ class TestBasic(TestCase):
         script = parser.get_script(buf)
         ann = script.annotations
         v0 = self.env.formula_manager.get_symbol('"v__AT0"')
-        v1_str = next(iter(ann[v0]["next"]))
-        self.assertEqual(v1_str, ":this_is_considered_a_value")
+        with self.assertRaises(StopIteration):
+            next(iter(ann[v0]["next"]))
+        with self.assertRaises(StopIteration):
+            next(iter(ann[v0]["this_is_considered_a_value"]))
 
 
 if __name__ == '__main__':