Always raise Unsat in Satml.assume if the environment is already (#…

…1301)

Fix a bug found while working on PR #1291. More precisely, the following script:
```ocaml
Options.set_interpretation ILast;
Options.set_debug_optimize true;
let x = Expr.mk_term (Symbols.name ~ns:User "x") [] Ty.Tint in
let gf = mk_gf Expr.Ints.(x <= ~$10) in
let env = SAT.empty () in
SAT.declare env (Hstring.make "x", [], Ty.Tint);
SAT.assume env gf Explanation.empty;
SAT.optimize env (Objective.Function.mk ~is_max:true x);
check_sat env;
SAT.assume env gf Explanation.empty; (* Should raise Unsat *)
check_sat env
```
did not raise unsat at the last `SAT.assume` but it should do it before merging #1291.

src/lib/reasoners/satml.ml

@@ -2144,6 +2144,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
 
 
   let assume env unit_cnf nunit_cnf f ~cnumber sff ~dec_lvl =
+    if env.is_unsat then raise (Unsat env.unsat_core);
     begin
       match unit_cnf, nunit_cnf with
       | [], [] -> ()