let init s = 
  icsat_initialize();    (* Initialize SAT solver *)
  Stack.clear stack;     (* Initialize stack *)
  Stack.push (s, []) stack;
  initial := (s, []);    (* Initial context *)
  scratch := s;          (* Initialize scratch area *)
  id := 0;               (* Initialize translation to props *)
  Atomtbl.clear atomtbl;
  Inttbl.clear inttbl;
  Atomtbl.clear idtbl;
  Nametbl.clear vartbl