Check that the matches len is correct

axiom-profiler-GUI/src/screen/inst_graph/display/node_info.rs

@@ -125,8 +125,8 @@ impl<'a, 'b> NodeInfo<'a, 'b> {
         let inst = self.node.kind().inst()?;
         let data = self.ctxt.parser.get_inst(inst);
         let qpat = data.match_.kind.quant_pat()?;
-        let pattern = self.ctxt.parser.get_pattern(qpat)?;
-        let pattern_matches = self.ctxt.parser[pattern]
+        let pattern = self.ctxt.parser.get_pattern_term(qpat)?;
+        let pattern_matches = pattern
             .child_ids
             .iter()
             .rev()

smt-log-parser/src/analysis/dependencies.rs

@@ -49,8 +49,8 @@ impl QuantifierAnalysis {
             let ginst = &inst_graph.raw[data.iidx];
             qinfo.costs += ginst.cost;
 
-            let pat = parser.get_pattern(qpat);
-            let subpats = pat.map(|p| parser[p].child_ids.len()).unwrap_or_default();
+            let pat = parser.get_pattern_term(qpat);
+            let subpats = pat.map(|p| p.child_ids.len()).unwrap_or_default();
             for (i, blame) in data.match_.pattern_matches().enumerate() {
                 // Increment the count for each expression in the pattern.
                 if i == qinfo.direct_deps.len() {

smt-log-parser/src/error.rs

@@ -56,6 +56,7 @@ pub enum Error {
     InvalidQVarInteger(ParseIntError),
     NewMatchOnLambda(QuantIdx),
     UnknownPatternIdx(TermIdx),
+    MatchPatternMismatch(usize, usize),
 
     // Inst discovered
     /// theory-solving non-rewrite axiom should blame valid enodes

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

@@ -727,6 +727,17 @@ impl Z3LogParser for Z3Parser {
             blamed: blamed.into(),
             frame: self.stack.active_frame(),
         };
+        // Z3 BUG: Sometimes the number of pattern_matches is larger than the
+        // number of subpatterns available.
+        let pat = QuantPat {
+            quant,
+            pat: Some(pattern),
+        };
+        let subpats = self.get_pattern_term(pat).unwrap().child_ids.len();
+        let subpat_matches = match_.pattern_matches().count();
+        if subpats != subpat_matches {
+            return Err(E::MatchPatternMismatch(subpats, subpat_matches));
+        }
         self.insts.new_match(fingerprint, match_)?;
         Ok(())
     }
@@ -1021,6 +1032,10 @@ impl Z3Parser {
         qpat.pat.map(|pat| self.patterns(qpat.quant).unwrap()[pat])
     }
 
+    pub fn get_pattern_term(&self, qpat: QuantPat) -> Option<&Term> {
+        self.get_pattern(qpat).map(|tidx| &self[tidx])
+    }
+
     pub fn get_frame(&self, idx: impl HasFrame) -> &StackFrame {
         &self.stack[idx.frame(self)]
     }