From f50cdfc9b6009d575a495b09be660dec6c701bc0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jon=C3=A1=C5=A1=20Fiala?= <jonas.fiala@inf.ethz.ch>
Date: Mon, 9 Dec 2024 14:58:20 +0100
Subject: [PATCH] Check that the matches blamed len is correct

---
 .../src/screen/inst_graph/display/node_info.rs    |  4 ++--
 smt-log-parser/src/analysis/dependencies.rs       |  4 ++--
 smt-log-parser/src/error.rs                       |  1 +
 smt-log-parser/src/parsers/z3/z3parser.rs         | 15 +++++++++++++++
 4 files changed, 20 insertions(+), 4 deletions(-)

diff --git a/axiom-profiler-GUI/src/screen/inst_graph/display/node_info.rs b/axiom-profiler-GUI/src/screen/inst_graph/display/node_info.rs
index 4341f0ed..a11e5c45 100644
--- a/axiom-profiler-GUI/src/screen/inst_graph/display/node_info.rs
+++ b/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()
diff --git a/smt-log-parser/src/analysis/dependencies.rs b/smt-log-parser/src/analysis/dependencies.rs
index 1f03cf49..d1c77bc1 100644
--- a/smt-log-parser/src/analysis/dependencies.rs
+++ b/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() {
diff --git a/smt-log-parser/src/error.rs b/smt-log-parser/src/error.rs
index 06c6f4fa..3c19abbb 100644
--- a/smt-log-parser/src/error.rs
+++ b/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
diff --git a/smt-log-parser/src/parsers/z3/z3parser.rs b/smt-log-parser/src/parsers/z3/z3parser.rs
index 8b4c3dd6..1897e3e5 100644
--- a/smt-log-parser/src/parsers/z3/z3parser.rs
+++ b/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)]
     }