Fix lib_usage and worker_js

examples/dune

@@ -0,0 +1,16 @@
+(executable
+ (name Lib_usage)
+ (libraries AltErgoLib)
+ (modules Lib_usage)
+)
+
+(rule
+ (alias runtest)
+ (action
+  (ignore-stdout
+   (ignore-stderr
+    (run ./Lib_usage.exe)
+   )
+  )
+ )
+)

examples/lib_usage.ml

@@ -65,7 +65,7 @@ open AltErgoLib
 
 module PA = Parsed_interface
 
-let x = PA.mk_var_type Loc.dummy "'a"
+let _x = PA.mk_var_type Loc.dummy "'a"
 
 let one = PA.mk_int_const Loc.dummy "1"
 let two = PA.mk_int_const Loc.dummy "2"
@@ -80,7 +80,7 @@ let goal_3 = PA.mk_goal Loc.dummy "toy_3" (PA.mk_not Loc.dummy eq1)
 
 let parsed = [goal_1; goal_2; goal_3]
 
-let typed, env = Typechecker.type_file parsed
+let typed, _env = Typechecker.type_file parsed
 
 let pbs = Typechecker.split_goals_and_cnf typed
 
@@ -89,16 +89,19 @@ module FE = Frontend.Make(SAT)
 
 let () =
   List.iter
-    (fun (pb, goal_name) ->
+    (fun (pb, _goal_name) ->
        let ctxt = FE.init_all_used_context () in
-       let acc0 = SAT.empty (), true, Explanation.empty in
+       let acc0 = SAT.empty (), `Unknown (SAT.empty ()), Explanation.empty in
        let s = Stack.create () in
-       let _, consistent, ex =
+       let _env, consistent, _ex =
          List.fold_left
            (fun acc d ->
               FE.process_decl (fun _ _ -> ()) ctxt s acc d
-           )acc0 pb
+           ) acc0 pb
        in
-       Format.printf "%s@."
-         (if consistent then "unknown" else "unsat")
+       match consistent with
+       | `Sat _ | `Unknown _ ->
+         Format.printf "unknown"
+       | `Unsat ->
+         Format.printf "unsat"
     )pbs

src/bin/js/worker_js.ml

@@ -130,11 +130,12 @@ let main worker_id content =
       let used_context = FE.choose_used_context all_context ~goal_name in
       let consistent_dep_stack = Stack.create () in
       SAT.reset_refs ();
+      let env = SAT.empty_with_inst add_inst in
       let _,_,dep =
         List.fold_left
           (FE.process_decl
              get_status_and_print used_context consistent_dep_stack)
-          (SAT.empty_with_inst add_inst, true, Explanation.empty) cnf in
+          (env, `Unknown env, Explanation.empty) cnf in
 
       if Options.get_unsat_core () then begin
         unsat_core := Explanation.get_unsat_core dep;