unit_tenv with ex

src/lib/reasoners/rel_utils.ml

@@ -303,7 +303,9 @@ end = struct
                       | Some deps ->
                         let deps = SX.remove r deps in
                         if SX.is_empty deps then None else Some deps
-                      | None -> assert false
+                      | None ->
+                        (* Can happen if the leaf is duplicated *)
+                        None
                     ) parents
               ) cgr.parents (X.leaves r)
           in

src/lib/reasoners/satml.ml

@@ -969,7 +969,12 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
            assert (ta.var.level >= 0);
            if ta.var.level <= Vec.size env.increm_guards then begin
              incr nb_f;
-             (ta.lit, Ex.empty, ta.var.level, env.cpt_current_propagations) :: acc
+             let ex =
+               if ta.var.level = 0 then Ex.empty else
+                 let d = Vec.get env.trail (Vec.get env.trail_lim (ta.var.level - 1)) in
+                 Ex.singleton (Ex.Literal d)
+             in
+             (ta.lit, ex, ta.var.level, env.cpt_current_propagations) :: acc
            end
            else acc
         )[] lazy_q

src/lib/reasoners/satml_frontend.ml

@@ -605,7 +605,7 @@ module Make (Th : Theory.S) : Sat_solver_sig.S = struct
         (fun f _ sa ->
            Debug.atoms_from_sat_branch f;
            match atoms_from_sat_branch f with
-           | None   -> sa (* TODO: can occur with incremental solving but maybe we want to make sure it doesn't *)
+           | None   -> assert false
            | Some l -> List.fold_left (fun sa a -> SE.add a sa) sa l
         ) env.conj SE.empty
 

tests/smtlib/testfile-get-info1.dolmen.expected

@@ -1,7 +1,7 @@
 
 unknown
 (
- :steps 10)
+ :steps 11)
 
 unsupported