From 596acf26ce68b053b7277e3159adc0110154d1a0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 16 Apr 2019 10:39:34 -0700
Subject: [PATCH] take second suggestion from #2234

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/opt/opt_parse.cpp | 28 +++++++++++++++++++++++-----
 1 file changed, 23 insertions(+), 5 deletions(-)

diff --git a/src/opt/opt_parse.cpp b/src/opt/opt_parse.cpp
index 215650300..2a8528ca3 100644
--- a/src/opt/opt_parse.cpp
+++ b/src/opt/opt_parse.cpp
@@ -687,14 +687,22 @@ private:
         return peek(pos) == "<=" || peek(pos) == "=<";
     }
 
-    bool peek_minus_infty(unsigned pos) {
+    bool peek_minus_infty_long(unsigned pos) {
         return peek(pos) == "-" && (peek(pos+1) == "inf" || peek(pos+1) == "infinity");
     }
 
-    bool peek_plus_infty(unsigned pos) {
+    bool peek_minus_infty_short(unsigned pos) {
+        return peek(pos) == "-inf" || peek(pos) == "-infinity";
+    }
+
+    bool peek_plus_infty_long(unsigned pos) {
         return peek(pos) == "+" && (peek(pos+1) == "inf" || peek(pos+1) == "infinity");
     }
 
+    bool peek_plus_infty_short(unsigned pos) {
+        return peek(pos) == "+inf" || peek(pos) == "+infinity";
+    }
+
     void parse_indicator(symbol& var, rational& val) {
         if (peek(1) == "=" && tok.peek_num(2) && peek(3) == "->") {
             var = peek(0);
@@ -731,14 +739,22 @@ private:
             tok.next(3);
             parse_upper(v);
         }
-        else if (peek_minus_infty(0) && peek_le(2)) {
+        else if (peek_minus_infty_long(0) && peek_le(2)) {
             v = peek(3);
             tok.next(4);
             parse_upper(v);
         }
-        else if (peek_plus_infty(2) && peek_le(1)) {
+        else if (peek_minus_infty_short(0) && peek_le(1)) {
+            v = peek(2);
+            tok.next(3);
+            parse_upper(v);
+        }
+        else if (peek_plus_infty_long(2) && peek_le(1)) {
             tok.next(4);            
         }
+        else if (peek_plus_infty_short(2) && peek_le(1)) {
+            tok.next(3);
+        }
         else if (peek_le(1) && tok.peek_num(2)) {
             v = peek(0);
             tok.next(2);
@@ -757,9 +773,11 @@ private:
             update_upper(v, rhs);
             tok.next(2);
         }
-        else if (peek_le(0) && peek_plus_infty(1)) {
+        else if (peek_le(0) && peek_plus_infty_long(1)) {
             tok.next(3);            
         }
+        else if (peek_le(0) && peek_plus_infty_short(1)) {
+            tok.next(2);        }
 
     }