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

@@ -710,12 +710,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(())