diff --git a/smt-log-parser/src/items.rs b/smt-log-parser/src/items.rs index dd52a2da..59ba4f5d 100644 --- a/smt-log-parser/src/items.rs +++ b/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(_)) diff --git a/smt-log-parser/src/parsers/z3/z3parser.rs b/smt-log-parser/src/parsers/z3/z3parser.rs index ff554b93..dc2813ac 100644 --- a/smt-log-parser/src/parsers/z3/z3parser.rs +++ b/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) -> 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::(); + // 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::(); + } + 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(); diff --git a/smt-log-parser/tests/parse_logs.rs b/smt-log-parser/tests/parse_logs.rs index dc6add15..49ea0558 100644 --- a/smt-log-parser/tests/parse_logs.rs +++ b/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()); }