Parser for counter-examples - bugfix.

src/driver/parse_smtv2_model.ml

@@ -73,8 +73,8 @@ let rec update_element_names_and_locations raw_model terms updated_model =
       
 (*
 *************************************************************** 
- **   Parser written using menhir 
- ****************************************************************
+**   Parser
+****************************************************************
 *)
 let get_position lexbuf =
   let pos = lexbuf.lex_curr_p in
@@ -107,9 +107,10 @@ let do_parsing model =
 let parse input printer_mapping =
   try
     let r = Str.regexp "unknown\\|sat" in
-    let start_m = Str.search_forward r input 0 in
+    ignore (Str.search_forward r input 0);
+    let match_end = Str.match_end () in
     let model_string = 
-      String.sub input start_m ((String.length input) - start_m) in
+      String.sub input match_end ((String.length input) - match_end) in
     
     let raw_model = do_parsing model_string in
     

src/driver/parse_smtv2_model_parser.mly

@@ -23,7 +23,7 @@ pairs:
 | possible_space { [] }
 | possible_space LPAREN term SPACE value RPAREN pairs 
     { (Model_parser.create_model_element ~name:$3 ~value:$5 ())::$7 }
-
+    
 possible_space:
 | { "" }
 | SPACE { $1 }
@@ -96,7 +96,7 @@ array:
     STORE possible_space array possible_space integer SPACE integer
     possible_space 
   RPAREN 
-	{ Model_parser.array_add_element ~array:$5 ~index:$7 ~value:$9 }
+    { Model_parser.array_add_element ~array:$5 ~index:$7 ~value:$9 }
 
 array_skipped_part:
 | LPAREN term_list RPAREN {}