Bodge to parse quantifier names with spaces

smt-log-parser/src/items.rs

@@ -128,7 +128,7 @@ impl QuantKind {
                 name: name.to_string(),
                 id,
             })
-            .unwrap_or_else(|| Self::NamedQuant(name.to_string()))
+            .unwrap_or_else(|| Self::NamedQuant(value.to_string()))
     }
     pub fn is_discovered(&self) -> bool {
         matches!(self, Self::Other(_))

smt-log-parser/src/parsers/z3/z3parser.rs

@@ -167,8 +167,17 @@ impl Z3LogParser for Z3Parser {
 
     fn mk_quant<'a>(&mut self, mut l: impl Iterator<Item = &'a str>) -> Option<()> {
         let full_id = l.next().and_then(TermIdCow::parse)?;
-        let quant_name = l.next().map(QuantKind::parse)?;
-        let num_vars = l.next()?.parse().ok()?;
+        let mut quant_name = std::borrow::Cow::Borrowed(l.next()?);
+        let mut num_vars_str = l.next()?;
+        let mut num_vars = num_vars_str.parse::<usize>();
+        // The name may contain spaces... TODO: PR to add quotes around name when logging in z3
+        while num_vars.is_err() {
+            quant_name = std::borrow::Cow::Owned(format!("{quant_name} {num_vars_str}"));
+            num_vars_str = l.next()?;
+            num_vars = num_vars_str.parse::<usize>();
+        }
+        let quant_name = QuantKind::parse(&*quant_name);
+        let num_vars = num_vars.unwrap();
         let children = self.gobble_children(l)?;
         assert!(!children.is_empty());
         let qidx = self.quantifiers.next_key();

smt-log-parser/tests/parse_logs.rs

@@ -11,8 +11,8 @@ fn parse_all_logs() {
         let filename = log.unwrap().path();
         println!("Parsing {}", filename.display());
         let (metadata, parser) = Z3Parser::from_file(filename).unwrap();
-        // Gives 20 millis per MB (or 20 secs per GB)
-        let to = Duration::from_millis(500 + (metadata.len() / 50_000));
+        // Gives 50 millis per MB (or 50 secs per GB)
+        let to = Duration::from_millis(500 + (metadata.len() / 20_000));
         let (timeout, _result) = parser.process_all_timeout(to);
         assert!(timeout.is_none());
     }