Undo reverted changes

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

@@ -153,6 +153,14 @@ impl VersionInfo {
         self.version()
             .is_some_and(|v| v == &semver::Version::new(major, minor, patch))
     }
+
+    pub fn is_version_minor(&self, major: u64, minor: u64) -> bool {
+        self.version().is_some_and(|v| {
+            &semver::Version::new(major, minor, 0) <= v
+                && v <= &semver::Version::new(major, minor, u64::MAX)
+        })
+    }
+
     pub fn is_ge_version(&self, major: u64, minor: u64, patch: u64) -> bool {
         self.version()
             .is_some_and(|v| v >= &semver::Version::new(major, minor, patch))

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

@@ -435,10 +435,7 @@ impl Z3LogParser for Z3Parser {
             .parse_existing_id(&mut self.strings, id)?;
         let qidx = self.terms.quant(tidx)?;
         assert!(self.quantifiers[qidx].vars.is_none());
-        assert!(!matches!(
-            self.quantifiers[qidx].kind,
-            QuantKind::Lambda { .. }
-        ));
+        assert!(!matches!(self.quantifiers[qidx].kind, QuantKind::Lambda(_)));
         self.quantifiers[qidx].vars = Some(var_names);
         Ok(())
     }
@@ -710,12 +707,12 @@ impl Z3LogParser for Z3Parser {
             z3_generation,
             yields_terms: Default::default(),
         };
-        // In version 4.12.2, I have on very rare occasions seen an `[instance]`
-        // repeated twice with the same fingerprint (without an intermediate
-        // `[new-match]`). We can try to remove the `can_duplicate` in the future.
-        let iidx =
-            self.insts
-                .new_inst(fingerprint, inst, self.version_info.is_version(4, 12, 2))?;
+        // In version 4.12.2 & 4.12.4, I have on very rare occasions seen an
+        // `[instance]` repeated twice with the same fingerprint (without an
+        // intermediate `[new-match]`). We can try to remove the `can_duplicate`
+        // in the future.
+        let can_duplicate = self.version_info.is_version_minor(4, 12);
+        let iidx = self.insts.new_inst(fingerprint, inst, can_duplicate)?;
         self.inst_stack.try_reserve(1)?;
         self.inst_stack.push((iidx, Vec::new()));
         Ok(())