let restore { env = s_env; st_cpt_mk_var = st_cpt_mk_var; st_ma = st_ma } = env.is_unsat <- s_env.is_unsat; env.unsat_core <- s_env.unsat_core; env.clauses <- s_env.clauses; env.learnts <- s_env.learnts; env.clause_inc <- s_env.clause_inc; env.var_inc <- s_env.var_inc; env.vars <- s_env.vars; env.qhead <- s_env.qhead; env.simpDB_assigns <- s_env.simpDB_assigns; env.simpDB_props <- s_env.simpDB_props; env.order <- s_env.order; env.progress_estimate <- s_env.progress_estimate; env.restart_first <- s_env.restart_first; env.starts <- s_env.starts; env.decisions <- s_env.decisions; env.propagations <- s_env.propagations; env.conflicts <- s_env.conflicts; env.clauses_literals <- s_env.clauses_literals; env.learnts_literals <- s_env.learnts_literals; env.max_literals <- s_env.max_literals; env.tot_literals <- s_env.tot_literals; env.nb_init_vars <- s_env.nb_init_vars; env.nb_init_clauses <- s_env.nb_init_clauses; env.tenv <- s_env.tenv; env.model <- s_env.model; env.trail <- s_env.trail; env.trail_lim <- s_env.trail_lim; env.tenv_queue <- s_env.tenv_queue; env.tatoms_queue <- s_env.tatoms_queue; Solver_types.cpt_mk_var := st_cpt_mk_var; Solver_types.ma := st_ma