Update ltl_infty branch

.github/workflows/rust.yml

@@ -0,0 +1,22 @@
+name: Rust
+
+on:
+  push:
+    branches: [ "main" ]
+  pull_request:
+    branches: [ "main" ]
+
+env:
+  CARGO_TERM_COLOR: always
+
+jobs:
+  build:
+
+    runs-on: ubuntu-latest
+
+    steps:
+    - uses: actions/checkout@v4
+    - name: Build
+      run: cargo build --verbose
+    - name: Run tests
+      run: cargo test --verbose

src/algos/meta/mod.rs

@@ -106,8 +106,14 @@ where
     let nb_traces = target.len();
     // Check whether the fom
     if let Some(f) = initial_cache.get_from_cv(target, target) {
-        debug!("Formula found in cache");
-        return Some(f);
+        // Due to hash collisions, the formula may not be right; we check that
+        // the formula has the right characteristic vector.
+        if f.eval(traces).accepted_vec() == target {
+            debug!("Formula found in cache");
+            return Some(f);
+        } else {
+            debug!("Hash collision found a wrong formula {f} for target {target:?}; continuing");
+        }
     }
     if nb_traces > 128 {
         split_and_solve_non_overlapping(traces, operators, initial_cache, target, params)