Decision level of SatML after calling unsat

[Halbaroth]

While implementing the get-value support (see #1032), I noticed that the decision level of SatML isn't always zero after calling SAT.unsat. It means we cannot always assert new facts after unsat if we use directly the SAT API of Alt-Ergo. A minimal example:

open AltErgoLib
module SAT = Satml_frontend.Make(Theory.Main_Default)

let assume env id e =
  SAT.assume env
    {Expr.ff= e;
     origin_name = id;
     gdist = -1;
     hdist = 0;
     trigger_depth = max_int;
     nb_reductions = 0;
     age=0;
     lem=None;
     mf=true;
     gf=false;
     from_terms = [];
     theory_elim = true;
    }
    Explanation.empty

let check env =
  try
    let ex = SAT.unsat env
        {Expr.ff=Expr.vrai;
         origin_name = "";
         hdist = -1;
         gdist = 0;
         trigger_depth = max_int;
         nb_reductions = 0;
         age=0;
         lem=None;
         mf=true;
         gf=true;
         from_terms = [];
         theory_elim = true;
        }
    in
    raise_notrace (SAT.Unsat ex)
  with
  | SAT.I_dont_know | SAT.Sat -> ()

let () =
  let p = Expr.mk_term (Symbols.name "p") [] Ty.Tbool in
  let q = Expr.mk_term (Symbols.name "q") [] Ty.Tbool in
  let imp = Expr.mk_imp p q in
  let env = SAT.empty () in
  assume env "foo" imp;
  try
    check env;
    let r = Expr.mk_term (Symbols.name "r") [] Ty.Tbool in
    assume env "boo" r;
    Format.printf "unknown@."
  with
  | SAT.Unsat _ -> Format.printf "unsat@."

The line assume env "boo" r raises the assertion:

assert (SAT.decision_level env.satml == 0);

This program behaves as expected if we replace SatML by FunSAT.