Merging upstream version 1.71.1+dfsg1.

Signed-off-by: Daniel Baumann <daniel.baumann@progress-linux.org>

12 files changed, 2808 insertions, 0 deletions

diff --git a/vendor/varisat-checker/src/clauses.rs b/vendor/varisat-checker/src/clauses.rs
new file mode 100644
index 000000000..06f99f4fd
--- /dev/null
+++ b/vendor/varisat-checker/src/clauses.rs
@@ -0,0 +1,453 @@
+//! Clause storage (unit and non-unit clauses).
+use std::{convert::TryInto, mem::transmute};
+
+use partial_ref::{partial, PartialRef};
+use rustc_hash::FxHashMap as HashMap;
+use smallvec::SmallVec;
+
+use varisat_formula::{lit::LitIdx, Lit};
+use varisat_internal_proof::ClauseHash;
+
+use crate::{
+    context::{parts::*, Context},
+    processing::{process_step, CheckedProofStep},
+    sorted_lits::copy_canonical,
+    variables::{ensure_sampling_var, ensure_var},
+    CheckerError,
+};
+
+const INLINE_LITS: usize = 3;
+
+/// Literals of a clause, either inline or an index into a buffer
+pub struct ClauseLits {
+    length: LitIdx,
+    inline: [LitIdx; INLINE_LITS],
+}
+
+impl ClauseLits {
+    /// Create a new ClauseLits, storing them in the given buffer if necessary
+    fn new(lits: &[Lit], buffer: &mut Vec<Lit>) -> ClauseLits {
+        let mut inline = [0; INLINE_LITS];
+        let length = lits.len();
+
+        if length > INLINE_LITS {
+            inline[0] = buffer
+                .len()
+                .try_into()
+                .expect("exceeded maximal literal buffer size");
+            buffer.extend(lits);
+        } else {
+            let lits = unsafe {
+                // Lit is a repr(transparent) wrapper of LitIdx
+                #[allow(clippy::transmute_ptr_to_ptr)]
+                transmute::<&[Lit], &[LitIdx]>(lits)
+            };
+            inline[..length].copy_from_slice(lits);
+        }
+
+        ClauseLits {
+            length: length as LitIdx,
+            inline,
+        }
+    }
+
+    /// Returns the literals as a slice given a storage buffer
+    pub fn slice<'a, 'b, 'c>(&'a self, buffer: &'b [Lit]) -> &'c [Lit]
+    where
+        'a: 'c,
+        'b: 'c,
+    {
+        if self.length > INLINE_LITS as LitIdx {
+            &buffer[self.inline[0] as usize..][..self.length as usize]
+        } else {
+            unsafe {
+                // Lit is a repr(transparent) wrapper of LitIdx
+                #[allow(clippy::transmute_ptr_to_ptr)]
+                transmute::<&[LitIdx], &[Lit]>(&self.inline[..self.length as usize])
+            }
+        }
+    }
+
+    /// Literals stored in the literal buffer
+    fn buffer_used(&self) -> usize {
+        if self.length > INLINE_LITS as LitIdx {
+            self.length as usize
+        } else {
+            0
+        }
+    }
+}
+
+/// Literals and metadata for non-unit clauses.
+pub struct Clause {
+    /// LRAT clause id.
+    pub id: u64,
+    /// How often the clause is present as irred., red. clause.
+    ///
+    /// For checking the formula is a multiset of clauses. This is necessary as the generating
+    /// solver might not check for duplicated clauses.
+    ref_count: [u32; 2],
+    /// Clause's literals.
+    pub lits: ClauseLits,
+}
+
+/// Identifies the origin of a unit clause.
+#[derive(Copy, Clone, Debug)]
+pub enum UnitId {
+    Global(u64),
+    TracePos(usize),
+    InClause,
+}
+
+/// Known unit clauses and metadata.
+#[derive(Copy, Clone, Debug)]
+pub struct UnitClause {
+    pub id: UnitId,
+    pub value: bool,
+}
+
+/// Return type of [`store_clause`]
+#[derive(Copy, Clone, PartialEq, Eq)]
+pub enum StoreClauseResult {
+    New,
+    Duplicate,
+    NewlyIrredundant,
+}
+
+/// Return type of [`delete_clause`]
+#[derive(Copy, Clone, PartialEq, Eq)]
+pub enum DeleteClauseResult {
+    Unchanged,
+    NewlyRedundant,
+    Removed,
+}
+/// Checker clause storage.
+#[derive(Default)]
+pub struct Clauses {
+    /// Next clause id to use.
+    pub next_clause_id: u64,
+    /// Literal storage for clauses,
+    pub literal_buffer: Vec<Lit>,
+    /// Number of literals in the buffer which are from deleted clauses.
+    garbage_size: usize,
+    /// Stores all known non-unit clauses indexed by their hash.
+    pub clauses: HashMap<ClauseHash, SmallVec<[Clause; 1]>>,
+    /// Stores known unit clauses and propagations during a clause check.
+    pub unit_clauses: Vec<Option<UnitClause>>,
+    /// This stores a conflict of input unit clauses.
+    ///
+    /// Our representation for unit clauses doesn't support conflicting units so this is used as a
+    /// workaround.
+    pub unit_conflict: Option<[u64; 2]>,
+}
+
+impl Clauses {
+    /// Value of a literal if known from unit clauses.
+    pub fn lit_value(&self, lit: Lit) -> Option<(bool, UnitClause)> {
+        self.unit_clauses[lit.index()]
+            .map(|unit_clause| (unit_clause.value ^ lit.is_negative(), unit_clause))
+    }
+}
+
+/// Adds a clause to the checker.
+pub fn add_clause<'a>(
+    mut ctx: partial!(Context<'a>, mut ClausesP, mut CheckerStateP, mut ProcessingP<'a>, mut TmpDataP, mut VariablesP, ClauseHasherP),
+    clause: &[Lit],
+) -> Result<(), CheckerError> {
+    if ctx.part(CheckerStateP).unsat {
+        return Ok(());
+    }
+
+    let (tmp_data, mut ctx) = ctx.split_part_mut(TmpDataP);
+
+    if copy_canonical(&mut tmp_data.tmp, clause) {
+        let (clauses, mut ctx) = ctx.split_part_mut(ClausesP);
+        process_step(
+            ctx.borrow(),
+            &CheckedProofStep::TautologicalClause {
+                id: clauses.next_clause_id,
+                clause: &tmp_data.tmp,
+            },
+        )?;
+        clauses.next_clause_id += 1;
+        return Ok(());
+    }
+
+    for &lit in tmp_data.tmp.iter() {
+        ensure_sampling_var(ctx.borrow(), lit.var())?;
+    }
+
+    let (id, added) = store_clause(ctx.borrow(), &tmp_data.tmp, false);
+
+    let (clauses, mut ctx) = ctx.split_part_mut(ClausesP);
+
+    match added {
+        StoreClauseResult::New => {
+            process_step(
+                ctx.borrow(),
+                &CheckedProofStep::AddClause {
+                    id,
+                    clause: &tmp_data.tmp,
+                },
+            )?;
+        }
+        StoreClauseResult::NewlyIrredundant | StoreClauseResult::Duplicate => {
+            if let StoreClauseResult::NewlyIrredundant = added {
+                process_step(
+                    ctx.borrow(),
+                    &CheckedProofStep::MakeIrredundant {
+                        id,
+                        clause: &tmp_data.tmp,
+                    },
+                )?;
+            }
+
+            process_step(
+                ctx.borrow(),
+                &CheckedProofStep::DuplicatedClause {
+                    id: clauses.next_clause_id,
+                    same_as_id: id,
+                    clause: &tmp_data.tmp,
+                },
+            )?;
+            // This is a duplicated clause. We want to ensure that the clause ids match the input
+            // order so we skip a clause id.
+            clauses.next_clause_id += 1;
+        }
+    }
+
+    Ok(())
+}
+
+/// Adds a clause to the checker data structures.
+///
+/// `lits` must be sorted and free of duplicates.
+///
+/// Returns the id of the added clause and indicates whether the clause is new or changed from
+/// redundant to irredundant.
+pub fn store_clause(
+    mut ctx: partial!(
+        Context,
+        mut CheckerStateP,
+        mut ClausesP,
+        mut VariablesP,
+        ClauseHasherP
+    ),
+    lits: &[Lit],
+    redundant: bool,
+) -> (u64, StoreClauseResult) {
+    for &lit in lits.iter() {
+        ensure_var(ctx.borrow(), lit.var());
+    }
+
+    match lits[..] {
+        [] => {
+            let id = ctx.part(ClausesP).next_clause_id;
+            ctx.part_mut(ClausesP).next_clause_id += 1;
+
+            ctx.part_mut(CheckerStateP).unsat = true;
+            (id, StoreClauseResult::New)
+        }
+        [lit] => store_unit_clause(ctx.borrow(), lit),
+        _ => {
+            let hash = ctx.part(ClauseHasherP).clause_hash(&lits);
+
+            let (clauses, mut ctx) = ctx.split_part_mut(ClausesP);
+
+            let candidates = clauses.clauses.entry(hash).or_default();
+
+            for candidate in candidates.iter_mut() {
+                if candidate.lits.slice(&clauses.literal_buffer) == &lits[..] {
+                    let result = if !redundant && candidate.ref_count[0] == 0 {
+                        // first irredundant copy
+                        StoreClauseResult::NewlyIrredundant
+                    } else {
+                        StoreClauseResult::Duplicate
+                    };
+
+                    let ref_count = &mut candidate.ref_count[redundant as usize];
+                    *ref_count = ref_count.checked_add(1).expect("ref_count overflow");
+                    return (candidate.id, result);
+                }
+            }
+
+            let id = clauses.next_clause_id;
+
+            let mut ref_count = [0, 0];
+            ref_count[redundant as usize] += 1;
+
+            candidates.push(Clause {
+                id,
+                ref_count,
+                lits: ClauseLits::new(&lits, &mut clauses.literal_buffer),
+            });
+
+            clauses.next_clause_id += 1;
+
+            for &lit in lits.iter() {
+                ctx.part_mut(VariablesP).lit_data[lit.code()].clause_count += 1;
+            }
+
+            (id, StoreClauseResult::New)
+        }
+    }
+}
+
+/// Adds a unit clause to the checker data structures.
+///
+/// Returns the id of the added clause and a boolean that is true if the clause wasn't already
+/// present.
+pub fn store_unit_clause(
+    mut ctx: partial!(Context, mut CheckerStateP, mut ClausesP),
+    lit: Lit,
+) -> (u64, StoreClauseResult) {
+    match ctx.part(ClausesP).lit_value(lit) {
+        Some((
+            true,
+            UnitClause {
+                id: UnitId::Global(id),
+                ..
+            },
+        )) => (id, StoreClauseResult::Duplicate),
+        Some((
+            false,
+            UnitClause {
+                id: UnitId::Global(conflicting_id),
+                ..
+            },
+        )) => {
+            ctx.part_mut(CheckerStateP).unsat = true;
+            let id = ctx.part(ClausesP).next_clause_id;
+            ctx.part_mut(ClausesP).unit_conflict = Some([conflicting_id, id]);
+            ctx.part_mut(ClausesP).next_clause_id += 1;
+            (id, StoreClauseResult::New)
+        }
+        Some(_) => unreachable!(),
+        None => {
+            let id = ctx.part(ClausesP).next_clause_id;
+
+            ctx.part_mut(ClausesP).unit_clauses[lit.index()] = Some(UnitClause {
+                value: lit.is_positive(),
+                id: UnitId::Global(id),
+            });
+
+            ctx.part_mut(ClausesP).next_clause_id += 1;
+
+            (id, StoreClauseResult::New)
+        }
+    }
+}
+
+/// Delete a clause from the current formula.
+///
+/// `lits` must be sorted and free of duplicates.
+///
+/// Returns the id of the deleted clause and whether the ref_count (or irredundant ref_count)
+/// became zero.
+pub fn delete_clause(
+    mut ctx: partial!(
+        Context,
+        mut ClausesP,
+        mut VariablesP,
+        CheckerStateP,
+        ClauseHasherP
+    ),
+    lits: &[Lit],
+    redundant: bool,
+) -> Result<(u64, DeleteClauseResult), CheckerError> {
+    if lits.len() < 2 {
+        return Err(CheckerError::check_failed(
+            ctx.part(CheckerStateP).step,
+            format!("delete of unit or empty clause {:?}", lits),
+        ));
+    }
+
+    let hash = ctx.part(ClauseHasherP).clause_hash(lits);
+
+    let clauses = ctx.part_mut(ClausesP);
+
+    let candidates = clauses.clauses.entry(hash).or_default();
+
+    let mut found = false;
+
+    let mut result = None;
+
+    let literal_buffer = &clauses.literal_buffer;
+    let garbage_size = &mut clauses.garbage_size;
+
+    candidates.retain(|candidate| {
+        if found || candidate.lits.slice(literal_buffer) != lits {
+            true
+        } else {
+            found = true;
+            let ref_count = &mut candidate.ref_count[redundant as usize];
+
+            if *ref_count == 0 {
+                true
+            } else {
+                *ref_count -= 1;
+
+                if candidate.ref_count == [0, 0] {
+                    *garbage_size += candidate.lits.buffer_used();
+                    result = Some((candidate.id, DeleteClauseResult::Removed));
+                    false
+                } else {
+                    if !redundant && candidate.ref_count[0] == 0 {
+                        result = Some((candidate.id, DeleteClauseResult::NewlyRedundant));
+                    } else {
+                        result = Some((candidate.id, DeleteClauseResult::Unchanged));
+                    }
+                    true
+                }
+            }
+        }
+    });
+
+    if candidates.is_empty() {
+        clauses.clauses.remove(&hash);
+    }
+
+    if let Some((_, DeleteClauseResult::Removed)) = result {
+        for &lit in lits.iter() {
+            ctx.part_mut(VariablesP).lit_data[lit.code()].clause_count -= 1;
+        }
+    }
+
+    if let Some(result) = result {
+        collect_garbage(ctx.borrow());
+        return Ok(result);
+    }
+
+    let msg = match (found, redundant) {
+        (false, _) => format!("delete of unknown clause {:?}", lits),
+        (_, true) => format!("delete of redundant clause {:?} which is irredundant", lits),
+        (_, false) => format!("delete of irredundant clause {:?} which is redundant", lits),
+    };
+    Err(CheckerError::check_failed(
+        ctx.part(CheckerStateP).step,
+        msg,
+    ))
+}
+
+/// Perform a garbage collection if required
+fn collect_garbage(mut ctx: partial!(Context, mut ClausesP)) {
+    let clauses = ctx.part_mut(ClausesP);
+    if clauses.garbage_size * 2 <= clauses.literal_buffer.len() {
+        return;
+    }
+
+    let mut new_buffer = vec![];
+
+    new_buffer.reserve(clauses.literal_buffer.len());
+
+    for (_, candidates) in clauses.clauses.iter_mut() {
+        for clause in candidates.iter_mut() {
+            let new_lits =
+                ClauseLits::new(clause.lits.slice(&clauses.literal_buffer), &mut new_buffer);
+            clause.lits = new_lits;
+        }
+    }
+
+    clauses.literal_buffer = new_buffer;
+    clauses.garbage_size = 0;
+}
diff --git a/vendor/varisat-checker/src/context.rs b/vendor/varisat-checker/src/context.rs
new file mode 100644
index 000000000..5cd7e807b
--- /dev/null
+++ b/vendor/varisat-checker/src/context.rs
@@ -0,0 +1,46 @@
+//! Central checker data structure.
+use partial_ref::{part, PartialRefTarget};
+
+use crate::{
+    clauses::Clauses, hash::ClauseHasher, processing::Processing, rup::RupCheck,
+    state::CheckerState, tmp::TmpData, variables::Variables,
+};
+
+/// Part declarations for the [`Context`] struct.
+pub mod parts {
+    use super::*;
+
+    part!(pub CheckerStateP: CheckerState);
+    part!(pub ClauseHasherP: ClauseHasher);
+    part!(pub ClausesP: Clauses);
+    part!(pub ProcessingP<'a>: Processing<'a>);
+    part!(pub RupCheckP: RupCheck);
+    part!(pub TmpDataP: TmpData);
+    part!(pub VariablesP: Variables);
+}
+
+use parts::*;
+
+/// Central checker data structure.
+///
+/// This struct contains all data kept by the checker. Most functions operating on multiple fields
+/// of the context use partial references provided by the `partial_ref` crate. This documents the
+/// data dependencies and makes the borrow checker happy without the overhead of passing individual
+/// references.
+#[derive(PartialRefTarget, Default)]
+pub struct Context<'a> {
+    #[part(CheckerStateP)]
+    pub checker_state: CheckerState,
+    #[part(ClauseHasherP)]
+    pub clause_hasher: ClauseHasher,
+    #[part(ClausesP)]
+    pub clauses: Clauses,
+    #[part(ProcessingP<'a>)]
+    pub processing: Processing<'a>,
+    #[part(RupCheckP)]
+    pub rup_check: RupCheck,
+    #[part(TmpDataP)]
+    pub tmp_data: TmpData,
+    #[part(VariablesP)]
+    pub variables: Variables,
+}
diff --git a/vendor/varisat-checker/src/hash.rs b/vendor/varisat-checker/src/hash.rs
new file mode 100644
index 000000000..40474ff8e
--- /dev/null
+++ b/vendor/varisat-checker/src/hash.rs
@@ -0,0 +1,74 @@
+//! Computation of clause hashes.
+use std::mem::take;
+
+use partial_ref::{partial, PartialRef};
+use rustc_hash::FxHashMap as HashMap;
+
+use varisat_formula::{Lit, Var};
+use varisat_internal_proof::{lit_code_hash, lit_hash, ClauseHash};
+
+use crate::context::{parts::*, Context};
+
+pub struct ClauseHasher {
+    /// How many bits are used for storing clause hashes.
+    pub hash_bits: u32,
+    /// Changed solver names that are not yet reflected in the checkers current clause hashes.
+    pub buffered_solver_var_names: Vec<(Var, Option<Var>)>,
+    /// Does buffered_solver_var_names contain a new name?
+    ///
+    /// If it contains only deletes, there is no need to rehash
+    pub rename_in_buffered_solver_var_names: bool,
+    /// Current mapping from global var names to solver var names, used for hashing.
+    solver_var_names: HashMap<Var, Var>,
+}
+
+impl Default for ClauseHasher {
+    fn default() -> ClauseHasher {
+        ClauseHasher {
+            hash_bits: 64,
+            buffered_solver_var_names: vec![],
+            rename_in_buffered_solver_var_names: false,
+            solver_var_names: Default::default(),
+        }
+    }
+}
+
+impl ClauseHasher {
+    /// Compute a clause hash of the current bit size
+    pub fn clause_hash(&self, lits: &[Lit]) -> ClauseHash {
+        let shift_bits = ClauseHash::max_value().count_ones() - self.hash_bits;
+        let mut hash = 0;
+        for &lit in lits.iter() {
+            match self.solver_var_names.get(&lit.var()) {
+                Some(var) => hash ^= lit_hash(var.lit(lit.is_positive())),
+                None => hash ^= lit_code_hash(lit.code() + Var::max_count() * 2),
+            }
+        }
+        hash >> shift_bits
+    }
+}
+
+/// Recompute all clause hashes if necessary
+pub fn rehash(mut ctx: partial!(Context, mut ClauseHasherP, mut ClausesP)) {
+    let (hasher, mut ctx) = ctx.split_part_mut(ClauseHasherP);
+    let clauses = ctx.part_mut(ClausesP);
+
+    for (global, solver) in hasher.buffered_solver_var_names.drain(..) {
+        if let Some(solver) = solver {
+            hasher.solver_var_names.insert(global, solver);
+        } else {
+            hasher.solver_var_names.remove(&global);
+        }
+    }
+    hasher.rename_in_buffered_solver_var_names = false;
+
+    let mut old_clauses = take(&mut clauses.clauses);
+
+    for (_, mut candidates) in old_clauses.drain() {
+        for clause in candidates.drain(..) {
+            let hash = hasher.clause_hash(clause.lits.slice(&clauses.literal_buffer));
+            let candidates = clauses.clauses.entry(hash).or_default();
+            candidates.push(clause);
+        }
+    }
+}
diff --git a/vendor/varisat-checker/src/internal.rs b/vendor/varisat-checker/src/internal.rs
new file mode 100644
index 000000000..5c13f0a03
--- /dev/null
+++ b/vendor/varisat-checker/src/internal.rs
@@ -0,0 +1,33 @@
+//! Varisat internal interface used for on-the-fly checking.
+
+use partial_ref::{IntoPartialRefMut, PartialRef};
+
+use varisat_internal_proof::ProofStep;
+
+use crate::{
+    state::{check_step, process_unit_conflicts},
+    Checker, CheckerError,
+};
+
+/// Varisat internal interface used for on-the-fly checking.
+///
+/// This should only be used within other Varisat crates. It is not considered part of the public
+/// API and may change at any time.
+pub trait SelfChecker {
+    fn self_check_step(&mut self, step: ProofStep) -> Result<(), CheckerError>;
+
+    fn self_check_delayed_steps(&mut self) -> Result<(), CheckerError>;
+}
+
+impl<'a> SelfChecker for Checker<'a> {
+    fn self_check_step(&mut self, step: ProofStep) -> Result<(), CheckerError> {
+        self.ctx.checker_state.step += 1;
+        let mut ctx = self.ctx.into_partial_ref_mut();
+        check_step(ctx.borrow(), step)
+    }
+
+    fn self_check_delayed_steps(&mut self) -> Result<(), CheckerError> {
+        let mut ctx = self.ctx.into_partial_ref_mut();
+        process_unit_conflicts(ctx.borrow())
+    }
+}
diff --git a/vendor/varisat-checker/src/lib.rs b/vendor/varisat-checker/src/lib.rs
new file mode 100644
index 000000000..22ff9f8ff
--- /dev/null
+++ b/vendor/varisat-checker/src/lib.rs
@@ -0,0 +1,773 @@
+//! Proof checker for Varisat proofs.
+
+use std::io;
+
+use anyhow::Error;
+use partial_ref::{IntoPartialRefMut, PartialRef};
+use thiserror::Error;
+
+use varisat_dimacs::DimacsParser;
+use varisat_formula::{CnfFormula, Lit};
+
+pub mod internal;
+
+mod clauses;
+mod context;
+mod hash;
+mod processing;
+mod rup;
+mod sorted_lits;
+mod state;
+mod tmp;
+mod transcript;
+mod variables;
+
+pub use processing::{
+    CheckedProofStep, CheckedSamplingMode, CheckedUserVar, CheckerData, ProofProcessor,
+    ResolutionPropagations,
+};
+pub use transcript::{ProofTranscriptProcessor, ProofTranscriptStep};
+
+use clauses::add_clause;
+use context::Context;
+use state::check_proof;
+
+/// Possible errors while checking a varisat proof.
+#[derive(Debug, Error)]
+#[non_exhaustive]
+pub enum CheckerError {
+    #[error("step {}: Unexpected end of proof file", step)]
+    ProofIncomplete { step: u64 },
+    #[error("step {}: Error reading proof file: {}", step, cause)]
+    IoError {
+        step: u64,
+        #[source]
+        cause: io::Error,
+    },
+    #[error("step {}: Could not parse proof step: {}", step, cause)]
+    ParseError {
+        step: u64,
+        #[source]
+        cause: Error,
+    },
+    #[error("step {}: Checking proof failed: {}", step, msg)]
+    CheckFailed {
+        step: u64,
+        msg: String,
+        debug_step: String,
+    },
+    #[error("Error in proof processor: {}", cause)]
+    ProofProcessorError {
+        #[source]
+        cause: Error,
+    },
+}
+
+impl CheckerError {
+    /// Generate a CheckFailed error with an empty debug_step
+    fn check_failed(step: u64, msg: String) -> CheckerError {
+        CheckerError::CheckFailed {
+            step,
+            msg,
+            debug_step: String::new(),
+        }
+    }
+}
+
+/// A checker for unsatisfiability proofs in the native varisat format.
+#[derive(Default)]
+pub struct Checker<'a> {
+    ctx: Box<Context<'a>>,
+}
+
+impl<'a> Checker<'a> {
+    /// Create a new checker.
+    pub fn new() -> Checker<'a> {
+        Checker::default()
+    }
+
+    /// Adds a clause to the checker.
+    pub fn add_clause(&mut self, clause: &[Lit]) -> Result<(), CheckerError> {
+        let mut ctx = self.ctx.into_partial_ref_mut();
+        add_clause(ctx.borrow(), clause)
+    }
+
+    /// Add a formula to the checker.
+    pub fn add_formula(&mut self, formula: &CnfFormula) -> Result<(), CheckerError> {
+        for clause in formula.iter() {
+            self.add_clause(clause)?;
+        }
+
+        Ok(())
+    }
+
+    /// Reads and adds a formula in DIMACS CNF format.
+    ///
+    /// Using this avoids creating a temporary [`CnfFormula`](varisat_formula::CnfFormula).
+    pub fn add_dimacs_cnf(&mut self, input: impl io::Read) -> Result<(), Error> {
+        let parser = DimacsParser::parse_incremental(input, |parser| {
+            Ok(self.add_formula(&parser.take_formula())?)
+        })?;
+
+        log::info!(
+            "Parsed formula with {} variables and {} clauses",
+            parser.var_count(),
+            parser.clause_count()
+        );
+
+        Ok(())
+    }
+
+    /// Add a [`ProofProcessor`].
+    ///
+    /// This has to be called before loading any clauses or checking any proofs.
+    pub fn add_processor(&mut self, processor: &'a mut dyn ProofProcessor) {
+        self.ctx.processing.processors.push(processor);
+    }
+
+    /// Add a [`ProofTranscriptProcessor`].
+    ///
+    /// This has to be called before loading any clauses or checking any proofs.
+    pub fn add_transcript(&mut self, processor: &'a mut dyn ProofTranscriptProcessor) {
+        self.ctx.processing.transcript_processors.push(processor);
+    }
+
+    /// Checks a proof in the native Varisat format.
+    pub fn check_proof(&mut self, input: impl io::Read) -> Result<(), CheckerError> {
+        let mut ctx = self.ctx.into_partial_ref_mut();
+        check_proof(ctx.borrow(), input)
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::{internal::SelfChecker, *};
+
+    use varisat_internal_proof::{DeleteClauseProof, ProofStep};
+
+    use varisat_formula::{cnf_formula, lits, Var};
+
+    fn expect_check_failed(result: Result<(), CheckerError>, contains: &str) {
+        match result {
+            Err(CheckerError::CheckFailed { ref msg, .. }) if msg.contains(contains) => (),
+            err => panic!("expected {:?} error but got {:?}", contains, err),
+        }
+    }
+
+    #[test]
+    fn conflicting_units() {
+        let mut checker = Checker::new();
+
+        checker
+            .add_formula(&cnf_formula![
+                1;
+                -1;
+            ])
+            .unwrap();
+
+        assert!(checker.ctx.checker_state.unsat);
+    }
+
+    #[test]
+    fn invalid_delete() {
+        let mut checker = Checker::new();
+
+        checker
+            .add_formula(&cnf_formula![
+                1, 2, 3;
+                -4, 5;
+            ])
+            .unwrap();
+
+        expect_check_failed(
+            checker.self_check_step(ProofStep::DeleteClause {
+                clause: &lits![-5, 4],
+                proof: DeleteClauseProof::Redundant,
+            }),
+            "unknown clause",
+        );
+    }
+
+    #[test]
+    fn ref_counts() {
+        let mut checker = Checker::new();
+
+        checker
+            .add_formula(&cnf_formula![
+                1, 2, 3;
+                1, 2, 3;
+                1;
+            ])
+            .unwrap();
+
+        let lits = &lits![1, 2, 3][..];
+
+        checker
+            .self_check_step(ProofStep::DeleteClause {
+                clause: lits,
+                proof: DeleteClauseProof::Satisfied,
+            })
+            .unwrap();
+
+        checker.add_clause(lits).unwrap();
+
+        checker
+            .self_check_step(ProofStep::DeleteClause {
+                clause: lits,
+                proof: DeleteClauseProof::Satisfied,
+            })
+            .unwrap();
+
+        checker
+            .self_check_step(ProofStep::DeleteClause {
+                clause: lits,
+                proof: DeleteClauseProof::Satisfied,
+            })
+            .unwrap();
+
+        expect_check_failed(
+            checker.self_check_step(ProofStep::DeleteClause {
+                clause: lits,
+                proof: DeleteClauseProof::Satisfied,
+            }),
+            "unknown clause",
+        );
+    }
+
+    #[test]
+    fn clause_not_found() {
+        let mut checker = Checker::new();
+        checker
+            .add_formula(&cnf_formula![
+                1, 2, 3;
+            ])
+            .unwrap();
+
+        expect_check_failed(
+            checker.self_check_step(ProofStep::AtClause {
+                redundant: false,
+                clause: [][..].into(),
+                propagation_hashes: [0][..].into(),
+            }),
+            "no clause found",
+        )
+    }
+
+    #[test]
+    fn clause_check_failed() {
+        let mut checker = Checker::new();
+        checker
+            .add_formula(&cnf_formula![
+                1, 2, 3;
+            ])
+            .unwrap();
+
+        expect_check_failed(
+            checker.self_check_step(ProofStep::AtClause {
+                redundant: false,
+                clause: [][..].into(),
+                propagation_hashes: [][..].into(),
+            }),
+            "AT check failed",
+        )
+    }
+
+    #[test]
+    fn add_derived_tautology() {
+        let mut checker = Checker::new();
+        checker
+            .add_formula(&cnf_formula![
+                1, 2, 3;
+            ])
+            .unwrap();
+
+        expect_check_failed(
+            checker.self_check_step(ProofStep::AtClause {
+                redundant: false,
+                clause: &lits![-3, 3],
+                propagation_hashes: &[],
+            }),
+            "tautology",
+        )
+    }
+
+    #[test]
+    fn delete_derived_tautology() {
+        let mut checker = Checker::new();
+        checker
+            .add_formula(&cnf_formula![
+                -3, 3;
+            ])
+            .unwrap();
+
+        expect_check_failed(
+            checker.self_check_step(ProofStep::DeleteClause {
+                clause: &lits![-3, 3],
+                proof: DeleteClauseProof::Redundant,
+            }),
+            "tautology",
+        )
+    }
+
+    #[test]
+    fn delete_unit_clause() {
+        let mut checker = Checker::new();
+        checker
+            .add_formula(&cnf_formula![
+                1;
+            ])
+            .unwrap();
+
+        expect_check_failed(
+            checker.self_check_step(ProofStep::DeleteClause {
+                clause: &lits![1],
+                proof: DeleteClauseProof::Redundant,
+            }),
+            "delete of unit or empty clause",
+        )
+    }
+
+    #[test]
+    fn delete_clause_not_redundant() {
+        let mut checker = Checker::new();
+        checker
+            .add_formula(&cnf_formula![
+                1, 2, 3;
+            ])
+            .unwrap();
+
+        expect_check_failed(
+            checker.self_check_step(ProofStep::DeleteClause {
+                clause: &lits![1, 2, 3],
+                proof: DeleteClauseProof::Redundant,
+            }),
+            "is irredundant",
+        )
+    }
+
+    #[test]
+    fn delete_clause_not_satisfied() {
+        let mut checker = Checker::new();
+        checker
+            .add_formula(&cnf_formula![
+                1, 2, 3;
+                -2;
+                4;
+            ])
+            .unwrap();
+
+        expect_check_failed(
+            checker.self_check_step(ProofStep::DeleteClause {
+                clause: &lits![1, 2, 3],
+                proof: DeleteClauseProof::Satisfied,
+            }),
+            "not satisfied",
+        )
+    }
+
+    #[test]
+    fn delete_clause_not_simplified() {
+        let mut checker = Checker::new();
+        checker
+            .add_formula(&cnf_formula![
+                1, 2, 3;
+                -3, 4;
+            ])
+            .unwrap();
+
+        let hashes = [
+            checker.ctx.clause_hasher.clause_hash(&lits![1, 2, 3]),
+            checker.ctx.clause_hasher.clause_hash(&lits![-3, 4]),
+        ];
+
+        checker
+            .self_check_step(ProofStep::AtClause {
+                redundant: false,
+                clause: &lits![1, 2, 4],
+                propagation_hashes: &hashes[..],
+            })
+            .unwrap();
+
+        expect_check_failed(
+            checker.self_check_step(ProofStep::DeleteClause {
+                clause: &lits![1, 2, 3],
+                proof: DeleteClauseProof::Simplified,
+            }),
+            "not subsumed",
+        )
+    }
+
+    #[test]
+    fn model_unit_conflict() {
+        let mut checker = Checker::new();
+        checker
+            .add_formula(&cnf_formula![
+                1;
+                2, 3;
+            ])
+            .unwrap();
+
+        expect_check_failed(
+            checker.self_check_step(ProofStep::Model {
+                assignment: &lits![-1, 2, -3],
+            }),
+            "conflicts with unit clause",
+        )
+    }
+
+    #[test]
+    fn model_internal_conflict() {
+        let mut checker = Checker::new();
+        checker
+            .add_formula(&cnf_formula![
+                2, 3;
+            ])
+            .unwrap();
+
+        expect_check_failed(
+            checker.self_check_step(ProofStep::Model {
+                assignment: &lits![-1, 1, 2, -3],
+            }),
+            "conflicting assignment",
+        )
+    }
+
+    #[test]
+    fn model_clause_unsat() {
+        let mut checker = Checker::new();
+        checker
+            .add_formula(&cnf_formula![
+                1, 2, 3;
+                -1, -2, 3;
+                1, -2, -3;
+            ])
+            .unwrap();
+
+        expect_check_failed(
+            checker.self_check_step(ProofStep::Model {
+                assignment: &lits![-1, 2, 3],
+            }),
+            "does not satisfy clause",
+        )
+    }
+    #[test]
+    fn model_conflicts_assumptions() {
+        let mut checker = Checker::new();
+        checker
+            .add_formula(&cnf_formula![
+                1, 2;
+                -1, 2;
+            ])
+            .unwrap();
+
+        checker
+            .self_check_step(ProofStep::Assumptions {
+                assumptions: &lits![-2],
+            })
+            .unwrap();
+
+        expect_check_failed(
+            checker.self_check_step(ProofStep::Model {
+                assignment: &lits![1, 2],
+            }),
+            "does not contain assumption",
+        )
+    }
+
+    #[test]
+    fn model_misses_assumption() {
+        let mut checker = Checker::new();
+        checker
+            .add_formula(&cnf_formula![
+                1, 2;
+                -1, 2;
+            ])
+            .unwrap();
+
+        checker
+            .self_check_step(ProofStep::Assumptions {
+                assumptions: &lits![-3],
+            })
+            .unwrap();
+
+        expect_check_failed(
+            checker.self_check_step(ProofStep::Model {
+                assignment: &lits![1, 2],
+            }),
+            "does not contain assumption",
+        )
+    }
+
+    #[test]
+    fn failed_core_with_non_assumed_vars() {
+        let mut checker = Checker::new();
+        checker
+            .add_formula(&cnf_formula![
+                1, 2;
+                -1, 2;
+            ])
+            .unwrap();
+
+        checker
+            .self_check_step(ProofStep::Assumptions {
+                assumptions: &lits![-2],
+            })
+            .unwrap();
+
+        expect_check_failed(
+            checker.self_check_step(ProofStep::FailedAssumptions {
+                failed_core: &lits![-2, -3],
+                propagation_hashes: &[],
+            }),
+            "contains non-assumed variables",
+        )
+    }
+
+    #[test]
+    fn failed_assumptions_with_missing_propagations() {
+        let mut checker = Checker::new();
+        checker
+            .add_formula(&cnf_formula![
+                1, 2;
+                -1, 2;
+                -3, -2;
+            ])
+            .unwrap();
+
+        checker
+            .self_check_step(ProofStep::Assumptions {
+                assumptions: &lits![3],
+            })
+            .unwrap();
+
+        expect_check_failed(
+            checker.self_check_step(ProofStep::FailedAssumptions {
+                failed_core: &lits![3],
+                propagation_hashes: &[],
+            }),
+            "AT check failed",
+        )
+    }
+
+    #[test]
+    fn failed_assumptions_with_conflicting_assumptions() {
+        let mut checker = Checker::new();
+        checker
+            .add_formula(&cnf_formula![
+                1, 2;
+                -1, 2;
+                -3, -2;
+            ])
+            .unwrap();
+
+        checker
+            .self_check_step(ProofStep::Assumptions {
+                assumptions: &lits![3, -3, 4],
+            })
+            .unwrap();
+
+        checker
+            .self_check_step(ProofStep::FailedAssumptions {
+                failed_core: &lits![3, -3],
+                propagation_hashes: &[],
+            })
+            .unwrap();
+    }
+
+    #[test]
+    fn add_clause_to_non_sampling_var() {
+        let mut checker = Checker::new();
+
+        checker
+            .self_check_step(ProofStep::ChangeSamplingMode {
+                var: Var::from_dimacs(1),
+                sample: false,
+            })
+            .unwrap();
+
+        expect_check_failed(
+            checker.self_check_step(ProofStep::AddClause {
+                clause: &lits![1, 2, 3],
+            }),
+            "not a sampling variable",
+        )
+    }
+
+    #[test]
+    fn add_clause_to_hidden_var() {
+        let mut checker = Checker::new();
+
+        checker
+            .self_check_step(ProofStep::UserVarName {
+                global: Var::from_dimacs(1),
+                user: Some(Var::from_dimacs(1)),
+            })
+            .unwrap();
+
+        checker
+            .self_check_step(ProofStep::UserVarName {
+                global: Var::from_dimacs(1),
+                user: None,
+            })
+            .unwrap();
+
+        expect_check_failed(
+            checker.self_check_step(ProofStep::AddClause {
+                clause: &lits![1, 2, 3],
+            }),
+            "not a sampling variable",
+        )
+    }
+
+    #[test]
+    fn colloding_user_vars() {
+        let mut checker = Checker::new();
+
+        checker
+            .self_check_step(ProofStep::UserVarName {
+                global: Var::from_dimacs(1),
+                user: Some(Var::from_dimacs(1)),
+            })
+            .unwrap();
+
+        expect_check_failed(
+            checker.self_check_step(ProofStep::UserVarName {
+                global: Var::from_dimacs(2),
+                user: Some(Var::from_dimacs(1)),
+            }),
+            "used for two different variables",
+        )
+    }
+
+    #[test]
+    fn observe_without_setting_mode() {
+        let mut checker = Checker::new();
+
+        checker
+            .self_check_step(ProofStep::UserVarName {
+                global: Var::from_dimacs(1),
+                user: Some(Var::from_dimacs(1)),
+            })
+            .unwrap();
+
+        checker
+            .self_check_step(ProofStep::UserVarName {
+                global: Var::from_dimacs(1),
+                user: None,
+            })
+            .unwrap();
+
+        expect_check_failed(
+            checker.self_check_step(ProofStep::UserVarName {
+                global: Var::from_dimacs(1),
+                user: Some(Var::from_dimacs(1)),
+            }),
+            "still hidden",
+        )
+    }
+
+    #[test]
+    fn hide_hidden_var() {
+        let mut checker = Checker::new();
+
+        checker
+            .self_check_step(ProofStep::UserVarName {
+                global: Var::from_dimacs(1),
+                user: Some(Var::from_dimacs(1)),
+            })
+            .unwrap();
+
+        checker
+            .self_check_step(ProofStep::UserVarName {
+                global: Var::from_dimacs(1),
+                user: None,
+            })
+            .unwrap();
+
+        expect_check_failed(
+            checker.self_check_step(ProofStep::UserVarName {
+                global: Var::from_dimacs(1),
+                user: None,
+            }),
+            "no user name to remove",
+        )
+    }
+
+    #[test]
+    fn delete_user_var() {
+        let mut checker = Checker::new();
+
+        checker
+            .self_check_step(ProofStep::UserVarName {
+                global: Var::from_dimacs(1),
+                user: Some(Var::from_dimacs(1)),
+            })
+            .unwrap();
+
+        expect_check_failed(
+            checker.self_check_step(ProofStep::DeleteVar {
+                var: Var::from_dimacs(1),
+            }),
+            "corresponds to user variable",
+        )
+    }
+
+    #[test]
+    fn delete_in_use_var() {
+        let mut checker = Checker::new();
+
+        checker
+            .self_check_step(ProofStep::UserVarName {
+                global: Var::from_dimacs(1),
+                user: Some(Var::from_dimacs(1)),
+            })
+            .unwrap();
+
+        checker
+            .self_check_step(ProofStep::AddClause {
+                clause: &lits![1, 2, 3],
+            })
+            .unwrap();
+
+        checker
+            .self_check_step(ProofStep::UserVarName {
+                global: Var::from_dimacs(1),
+                user: None,
+            })
+            .unwrap();
+
+        expect_check_failed(
+            checker.self_check_step(ProofStep::DeleteVar {
+                var: Var::from_dimacs(1),
+            }),
+            "still has clauses",
+        )
+    }
+
+    #[test]
+    fn invalid_hidden_to_sample() {
+        let mut checker = Checker::new();
+
+        checker
+            .self_check_step(ProofStep::UserVarName {
+                global: Var::from_dimacs(1),
+                user: Some(Var::from_dimacs(1)),
+            })
+            .unwrap();
+
+        checker
+            .self_check_step(ProofStep::UserVarName {
+                global: Var::from_dimacs(1),
+                user: None,
+            })
+            .unwrap();
+
+        expect_check_failed(
+            checker.self_check_step(ProofStep::ChangeSamplingMode {
+                var: Var::from_dimacs(1),
+                sample: true,
+            }),
+            "cannot sample hidden variable",
+        )
+    }
+}
diff --git a/vendor/varisat-checker/src/processing.rs b/vendor/varisat-checker/src/processing.rs
new file mode 100644
index 000000000..038406cca
--- /dev/null
+++ b/vendor/varisat-checker/src/processing.rs
@@ -0,0 +1,189 @@
+//! Processing of checked proof steps.
+use partial_ref::{partial, PartialRef};
+
+use anyhow::Error;
+use varisat_formula::{Lit, Var};
+
+use crate::{
+    context::{parts::*, Context},
+    transcript::{self, ProofTranscriptProcessor},
+    variables::SamplingMode,
+    CheckerError,
+};
+
+/// A single step of a proof.
+///
+/// Clauses are identified by a unique increasing id assigned by the checker. Whenever the literals
+/// of a clause are included in a step, they are sorted and free of duplicates.
+#[derive(Debug)]
+pub enum CheckedProofStep<'a> {
+    /// Updates the corresponding user variable for a proof variable.
+    UserVar {
+        var: Var,
+        user_var: Option<CheckedUserVar>,
+    },
+    /// A clause of the input formula.
+    AddClause { id: u64, clause: &'a [Lit] },
+    /// A duplicated clause of the input formula.
+    ///
+    /// The checker detects duplicated clauses and will use the same id for all copies. This also
+    /// applies to clauses of the input formula. This step allows proof processors to identify the
+    /// input formula's clauses by consecutive ids. When a duplicate clause is found, an id is
+    /// allocated and this step is emitted. The duplicated clause is not considered part of the
+    /// formula and the allocated id will not be used in any other steps.
+    DuplicatedClause {
+        id: u64,
+        same_as_id: u64,
+        clause: &'a [Lit],
+    },
+    /// A tautological clause of the input formula.
+    ///
+    /// Tautological clauses can be completely ignored. This step is only used to give an id to a
+    /// tautological input clause.
+    TautologicalClause { id: u64, clause: &'a [Lit] },
+    /// Addition of an asymmetric tautology (AT).
+    ///
+    /// A clause C is an asymmetric tautology wrt. a formula F, iff unit propagation in F with the
+    /// negated literals of C as unit clauses leads to a conflict. The `propagations` field contains
+    /// clauses in the order they became unit and as last element the clause that caused a conflict.
+    AtClause {
+        id: u64,
+        redundant: bool,
+        clause: &'a [Lit],
+        propagations: &'a [u64],
+    },
+    /// Deletion of a redundant clause.
+    DeleteClause { id: u64, clause: &'a [Lit] },
+    /// Deletion of a clause that is an asymmetric tautology w.r.t the remaining irredundant
+    /// clauses.
+    DeleteAtClause {
+        id: u64,
+        keep_as_redundant: bool,
+        clause: &'a [Lit],
+        propagations: &'a [u64],
+    },
+    /// Deletion of a resolution asymmetric tautology w.r.t the remaining irredundant caluses.
+    ///
+    /// The pivot is always a hidden variable.
+    DeleteRatClause {
+        id: u64,
+        keep_as_redundant: bool,
+        clause: &'a [Lit],
+        pivot: Lit,
+        propagations: &'a ResolutionPropagations,
+    },
+    /// Make a redundant clause irredundant.
+    MakeIrredundant { id: u64, clause: &'a [Lit] },
+    /// A (partial) assignment that satisfies all clauses and assumptions.
+    Model { assignment: &'a [Lit] },
+    /// Change the active set of assumptions.
+    Assumptions { assumptions: &'a [Lit] },
+    /// Subset of assumptions incompatible with the formula.
+    ///
+    /// The proof consists of showing that the negation of the assumptions is an AT wrt. the
+    /// formula.
+    FailedAssumptions {
+        failed_core: &'a [Lit],
+        propagations: &'a [u64],
+    },
+}
+
+/// Sampling mode of a user variable.
+#[derive(Debug)]
+pub enum CheckedSamplingMode {
+    Sample,
+    Witness,
+}
+
+/// Corresponding user variable for a proof variable.
+#[derive(Debug)]
+pub struct CheckedUserVar {
+    pub user_var: Var,
+    pub sampling_mode: CheckedSamplingMode,
+    pub new_var: bool,
+}
+
+/// A list of clauses to resolve and propagations to show that the resolvent is an AT.
+#[derive(Debug)]
+pub struct ResolutionPropagations {
+    // TODO implement ResolutionPropagations
+}
+
+/// Checker data available to proof processors.
+#[derive(Copy, Clone)]
+pub struct CheckerData<'a, 'b>(pub partial!('a Context<'b>, VariablesP));
+
+impl<'a, 'b> CheckerData<'a, 'b> {
+    /// User variable corresponding to proof variable.
+    ///
+    /// Returns `None` if the proof variable is an internal or hidden variable.
+    pub fn user_from_proof_var(self, proof_var: Var) -> Option<Var> {
+        let variables = self.0.part(VariablesP);
+        variables
+            .var_data
+            .get(proof_var.index())
+            .and_then(|var_data| {
+                var_data.user_var.or_else(|| {
+                    // This is needed as yet another workaround to enable independently loading the
+                    // initial formula and proof.
+                    // TODO can this be solved in a better way?
+                    if var_data.sampling_mode == SamplingMode::Sample {
+                        Some(proof_var)
+                    } else {
+                        None
+                    }
+                })
+            })
+    }
+}
+
+/// Implement to process proof steps.
+pub trait ProofProcessor {
+    fn process_step(&mut self, step: &CheckedProofStep, data: CheckerData) -> Result<(), Error>;
+}
+
+/// Registry of proof and transcript processors.
+#[derive(Default)]
+pub struct Processing<'a> {
+    /// Registered proof processors.
+    pub processors: Vec<&'a mut dyn ProofProcessor>,
+    /// Registered transcript processors.
+    pub transcript_processors: Vec<&'a mut dyn ProofTranscriptProcessor>,
+    /// Proof step to transcript step conversion.
+    transcript: transcript::Transcript,
+}
+
+impl<'a> Processing<'a> {
+    /// Process a single step
+    pub fn step<'b>(
+        &mut self,
+        step: &CheckedProofStep<'b>,
+        data: CheckerData,
+    ) -> Result<(), CheckerError> {
+        for processor in self.processors.iter_mut() {
+            if let Err(err) = processor.process_step(step, data) {
+                return Err(CheckerError::ProofProcessorError { cause: err });
+            }
+        }
+        if !self.transcript_processors.is_empty() {
+            if let Some(transcript_step) = self.transcript.transcript_step(step, data) {
+                for processor in self.transcript_processors.iter_mut() {
+                    if let Err(err) = processor.process_step(&transcript_step) {
+                        return Err(CheckerError::ProofProcessorError { cause: err });
+                    }
+                }
+            }
+        }
+
+        Ok(())
+    }
+}
+
+/// Process a single step
+pub fn process_step<'a, 'b>(
+    mut ctx: partial!(Context<'a>, mut ProcessingP<'a>, VariablesP),
+    step: &CheckedProofStep<'b>,
+) -> Result<(), CheckerError> {
+    let (processing, mut ctx) = ctx.split_part_mut(ProcessingP);
+    processing.step(step, CheckerData(ctx.borrow()))
+}
diff --git a/vendor/varisat-checker/src/rup.rs b/vendor/varisat-checker/src/rup.rs
new file mode 100644
index 000000000..e6f2b9f03
--- /dev/null
+++ b/vendor/varisat-checker/src/rup.rs
@@ -0,0 +1,203 @@
+//! Reverse unit propagation redundancy checks.
+use std::ops::Range;
+
+use partial_ref::{partial, PartialRef};
+
+use varisat_formula::{lit::LitIdx, Lit};
+use varisat_internal_proof::ClauseHash;
+
+use crate::{
+    clauses::{UnitClause, UnitId},
+    context::{parts::*, Context},
+    hash::rehash,
+    variables::ensure_var,
+    CheckerError,
+};
+
+/// Propagation of the RUP check.
+struct TraceItem {
+    id: u64,
+    edges: Range<usize>,
+    unused: bool,
+}
+
+#[derive(Default)]
+pub struct RupCheck {
+    /// Stores overwritten values in `unit_clauses` to undo assignments.
+    trail: Vec<(Lit, Option<UnitClause>)>,
+    /// Involved clauses during the last check.
+    trace: Vec<TraceItem>,
+    /// Edges of the trace implication graph.
+    trace_edges: Vec<LitIdx>,
+    /// Just the ids of `trace`.
+    pub trace_ids: Vec<u64>,
+}
+
+/// Check whether a clause is implied by clauses of the given hashes.
+///
+/// `lits` must be sorted and free of duplicates.
+pub fn check_clause_with_hashes<'a>(
+    mut ctx: partial!(
+        Context<'a>,
+        mut ClauseHasherP,
+        mut ClausesP,
+        mut ProcessingP<'a>,
+        mut RupCheckP,
+        mut VariablesP,
+        CheckerStateP,
+    ),
+    lits: &[Lit],
+    propagation_hashes: &[ClauseHash],
+) -> Result<(), CheckerError> {
+    if ctx.part(ClauseHasherP).rename_in_buffered_solver_var_names {
+        // TODO partial rehashing?
+        rehash(ctx.borrow());
+    }
+
+    let (rup, mut ctx) = ctx.split_part_mut(RupCheckP);
+
+    rup.trace.clear();
+    rup.trace_edges.clear();
+
+    let mut rup_is_unsat = false;
+
+    assert!(rup.trail.is_empty());
+
+    for &lit in lits.iter() {
+        ensure_var(ctx.borrow(), lit.var());
+    }
+
+    let (clauses, ctx) = ctx.split_part_mut(ClausesP);
+
+    for &lit in lits.iter() {
+        if let Some((true, unit)) = clauses.lit_value(lit) {
+            if let UnitId::Global(id) = unit.id {
+                rup.trace_ids.clear();
+                rup.trace_ids.push(id);
+                return Ok(());
+            } else {
+                unreachable!("unexpected non global unit");
+            }
+        }
+    }
+
+    // Set all lits to false
+    for &lit in lits.iter() {
+        rup.trail.push((lit, clauses.unit_clauses[lit.index()]));
+
+        clauses.unit_clauses[lit.index()] = Some(UnitClause {
+            value: lit.is_negative(),
+            id: UnitId::InClause,
+        });
+    }
+
+    'hashes: for &hash in propagation_hashes.iter() {
+        let candidates = match clauses.clauses.get(&hash) {
+            Some(candidates) if !candidates.is_empty() => candidates,
+            _ => {
+                return Err(CheckerError::check_failed(
+                    ctx.part(CheckerStateP).step,
+                    format!("no clause found for hash {:x}", hash),
+                ))
+            }
+        };
+
+        // Check if any clause matching the hash propagates
+        'candidates: for clause in candidates.iter() {
+            let mut unassigned_count = 0;
+            let mut unassigned_lit = None;
+
+            let range_begin = rup.trace_edges.len();
+
+            for &lit in clause.lits.slice(&clauses.literal_buffer).iter() {
+                match clauses.lit_value(lit) {
+                    Some((true, _)) => {
+                        continue 'candidates;
+                    }
+                    Some((false, unit)) => match unit.id {
+                        UnitId::Global(id) => {
+                            rup.trail.push((lit, clauses.unit_clauses[lit.index()]));
+                            clauses.unit_clauses[lit.index()] = Some(UnitClause {
+                                value: lit.is_negative(),
+                                id: UnitId::TracePos(rup.trace.len()),
+                            });
+
+                            rup.trace_edges.push(rup.trace.len() as LitIdx);
+
+                            rup.trace.push(TraceItem {
+                                id,
+                                edges: 0..0,
+                                unused: true,
+                            });
+                        }
+                        UnitId::TracePos(pos) => {
+                            rup.trace_edges.push(pos as LitIdx);
+                        }
+                        UnitId::InClause => {}
+                    },
+                    None => {
+                        unassigned_count += 1;
+                        unassigned_lit = Some(lit);
+                    }
+                }
+            }
+
+            let range = range_begin..rup.trace_edges.len();
+
+            match unassigned_lit {
+                None => {
+                    rup.trace.push(TraceItem {
+                        id: clause.id,
+                        edges: range,
+                        unused: false,
+                    });
+
+                    rup_is_unsat = true;
+                    break 'hashes;
+                }
+                Some(lit) if unassigned_count == 1 => {
+                    rup.trail.push((lit, clauses.unit_clauses[lit.index()]));
+
+                    clauses.unit_clauses[lit.index()] = Some(UnitClause {
+                        value: lit.is_positive(),
+                        id: UnitId::TracePos(rup.trace.len()),
+                    });
+
+                    rup.trace.push(TraceItem {
+                        id: clause.id,
+                        edges: range,
+                        unused: true,
+                    });
+                }
+                _ => (),
+            }
+        }
+    }
+
+    if rup_is_unsat && !ctx.part(ProcessingP).processors.is_empty() {
+        for i in (0..rup.trace.len()).rev() {
+            if !rup.trace[i].unused {
+                let edges = rup.trace[i].edges.clone();
+                for &edge in rup.trace_edges[edges].iter() {
+                    rup.trace[edge as usize].unused = false;
+                }
+            }
+        }
+        rup.trace_ids.clear();
+        rup.trace_ids.extend(rup.trace.iter().map(|trace| trace.id));
+    }
+
+    // Undo temporary assignments
+    for (lit, value) in rup.trail.drain(..).rev() {
+        clauses.unit_clauses[lit.index()] = value;
+    }
+
+    if rup_is_unsat {
+        Ok(())
+    } else {
+        Err(CheckerError::check_failed(
+            ctx.part(CheckerStateP).step,
+            format!("AT check failed for {:?}", lits),
+        ))
+    }
+}
diff --git a/vendor/varisat-checker/src/sorted_lits.rs b/vendor/varisat-checker/src/sorted_lits.rs
new file mode 100644
index 000000000..3c9e12e63
--- /dev/null
+++ b/vendor/varisat-checker/src/sorted_lits.rs
@@ -0,0 +1,56 @@
+//! Utilities for slices of sorted literals.
+use std::cmp::Ordering;
+
+use varisat_formula::Lit;
+
+/// Sort literals, remove duplicates and check for tautologic clauses.
+///
+/// Return true if the clause is a tautology
+pub fn copy_canonical(target: &mut Vec<Lit>, src: &[Lit]) -> bool {
+    target.clear();
+    target.extend_from_slice(src);
+    target.sort();
+    target.dedup();
+
+    let mut last = None;
+
+    target.iter().any(|&lit| {
+        let tautology = last == Some(!lit);
+        last = Some(lit);
+        tautology
+    })
+}
+
+/// Test whether a set of literals is a (strict) subset of another set of literals
+///
+/// Requires subset and superset to be sorted.
+pub fn is_subset(mut subset: &[Lit], mut superset: &[Lit], strict: bool) -> bool {
+    // We set is_strict to true if we don't require a strict subset
+    let mut is_strict = !strict;
+
+    while let Some((&sub_min, sub_rest)) = subset.split_first() {
+        if let Some((&super_min, super_rest)) = superset.split_first() {
+            match sub_min.cmp(&super_min) {
+                Ordering::Less => {
+                    // sub_min is not in superset
+                    return false;
+                }
+                Ordering::Greater => {
+                    // super_min is not in subset, skip it
+                    superset = super_rest;
+                    is_strict = true;
+                }
+                Ordering::Equal => {
+                    // sub_min == super_min, go to next element
+                    superset = super_rest;
+                    subset = sub_rest;
+                }
+            }
+        } else {
+            // sub_min is not in superset
+            return false;
+        }
+    }
+    is_strict |= !superset.is_empty();
+    is_strict
+}
diff --git a/vendor/varisat-checker/src/state.rs b/vendor/varisat-checker/src/state.rs
new file mode 100644
index 000000000..7f3e7478f
--- /dev/null
+++ b/vendor/varisat-checker/src/state.rs
@@ -0,0 +1,645 @@
+//! Checker state and checking of proof steps.
+
+use std::{io, mem::replace};
+
+use partial_ref::{partial, PartialRef};
+use rustc_hash::FxHashSet as HashSet;
+
+use varisat_formula::{Lit, Var};
+use varisat_internal_proof::{binary_format::Parser, ClauseHash, DeleteClauseProof, ProofStep};
+
+use crate::{
+    clauses::{
+        add_clause, delete_clause, store_clause, store_unit_clause, DeleteClauseResult,
+        StoreClauseResult, UnitClause, UnitId,
+    },
+    context::{parts::*, Context},
+    hash::rehash,
+    processing::{
+        process_step, CheckedProofStep, CheckedSamplingMode, CheckedUserVar, ResolutionPropagations,
+    },
+    rup::check_clause_with_hashes,
+    sorted_lits::{copy_canonical, is_subset},
+    variables::{
+        add_user_mapping, ensure_sampling_var, ensure_var, remove_user_mapping, SamplingMode,
+        VarData,
+    },
+    CheckerError,
+};
+
+/// A checker for unsatisfiability proofs in the native varisat format.
+#[derive(Default)]
+pub struct CheckerState {
+    /// Current step number.
+    pub step: u64,
+    /// Whether unsatisfiability was proven.
+    pub unsat: bool,
+    /// Whether an end of proof step was checked.
+    ended: bool,
+    /// Last added irredundant clause id.
+    ///
+    /// Sorted and free of duplicates.
+    previous_irred_clause_id: Option<u64>,
+    /// Last added irredundant clause literals.
+    previous_irred_clause_lits: Vec<Lit>,
+    /// Current assumptions, used to check FailedAssumptions and Model
+    assumptions: Vec<Lit>,
+}
+
+impl CheckerState {
+    /// Check whether a given clause is subsumed by the last added irredundant clause.
+    ///
+    /// `lits` must be sorted and free of duplicates.
+    fn subsumed_by_previous_irred_clause(&self, lits: &[Lit]) -> bool {
+        if self.previous_irred_clause_id.is_none() {
+            return false;
+        }
+        is_subset(&self.previous_irred_clause_lits[..], lits, true)
+    }
+}
+
+/// Check a single proof step
+pub fn check_step<'a>(
+    mut ctx: partial!(
+        Context<'a>,
+        mut CheckerStateP,
+        mut ClauseHasherP,
+        mut ClausesP,
+        mut ProcessingP<'a>,
+        mut RupCheckP,
+        mut TmpDataP,
+        mut VariablesP,
+    ),
+    step: ProofStep,
+) -> Result<(), CheckerError> {
+    let mut result = match step {
+        ProofStep::SolverVarName { global, solver } => {
+            ctx.part_mut(ClauseHasherP)
+                .buffered_solver_var_names
+                .push((global, solver));
+            if solver.is_some() {
+                ctx.part_mut(ClauseHasherP)
+                    .rename_in_buffered_solver_var_names = true;
+            }
+            Ok(())
+        }
+        ProofStep::UserVarName { global, user } => {
+            if let Some(user) = user {
+                add_user_mapping(ctx.borrow(), global, user)?;
+            } else {
+                remove_user_mapping(ctx.borrow(), global)?;
+            }
+            Ok(())
+        }
+        ProofStep::DeleteVar { var } => check_delete_var_step(ctx.borrow(), var),
+        ProofStep::ChangeSamplingMode { var, sample } => {
+            check_change_sampling_mode(ctx.borrow(), var, sample)
+        }
+        ProofStep::AddClause { clause } => add_clause(ctx.borrow(), clause),
+        ProofStep::AtClause {
+            redundant,
+            clause,
+            propagation_hashes,
+        } => check_at_clause_step(ctx.borrow(), redundant, clause, propagation_hashes),
+        ProofStep::DeleteClause { clause, proof } => {
+            check_delete_clause_step(ctx.borrow(), clause, proof)
+        }
+        ProofStep::UnitClauses { units } => check_unit_clauses_step(ctx.borrow(), units),
+        ProofStep::ChangeHashBits { bits } => {
+            ctx.part_mut(ClauseHasherP).hash_bits = bits;
+            rehash(ctx.borrow());
+            Ok(())
+        }
+        ProofStep::Model { assignment } => check_model_step(ctx.borrow(), assignment),
+        ProofStep::Assumptions { assumptions } => {
+            for &lit in assumptions.iter() {
+                ensure_sampling_var(ctx.borrow(), lit.var())?;
+            }
+            copy_canonical(&mut ctx.part_mut(CheckerStateP).assumptions, assumptions);
+
+            let (state, mut ctx) = ctx.split_part(CheckerStateP);
+
+            process_step(
+                ctx.borrow(),
+                &CheckedProofStep::Assumptions {
+                    assumptions: &state.assumptions,
+                },
+            )?;
+            Ok(())
+        }
+        ProofStep::FailedAssumptions {
+            failed_core,
+            propagation_hashes,
+        } => check_failed_assumptions_step(ctx.borrow(), failed_core, propagation_hashes),
+        ProofStep::End => {
+            ctx.part_mut(CheckerStateP).ended = true;
+            Ok(())
+        }
+    };
+
+    if let Err(CheckerError::CheckFailed {
+        ref mut debug_step, ..
+    }) = result
+    {
+        *debug_step = format!("{:?}", step)
+    }
+    result
+}
+
+/// Check a DeleteVar step
+fn check_delete_var_step<'a>(
+    mut ctx: partial!(
+        Context<'a>,
+        mut ClausesP,
+        mut ProcessingP<'a>,
+        mut VariablesP,
+        CheckerStateP,
+    ),
+    var: Var,
+) -> Result<(), CheckerError> {
+    ensure_var(ctx.borrow(), var);
+    if let Some(user_var) = ctx.part(VariablesP).var_data[var.index()].user_var {
+        return Err(CheckerError::check_failed(
+            ctx.part(CheckerStateP).step,
+            format!(
+                "deleted variable {:?} corresponds to user variable {:?}",
+                var, user_var
+            ),
+        ));
+    }
+
+    for &polarity in &[false, true] {
+        if ctx.part(VariablesP).lit_data[var.lit(polarity).code()].clause_count > 0 {
+            return Err(CheckerError::check_failed(
+                ctx.part(CheckerStateP).step,
+                format!("deleted variable {:?} still has clauses", var),
+            ));
+        }
+    }
+
+    if let Some(unit_clause) = ctx.part(ClausesP).unit_clauses[var.index()] {
+        let clause = [var.lit(unit_clause.value)];
+
+        let id = match unit_clause.id {
+            UnitId::Global(id) => id,
+            _ => unreachable!(),
+        };
+
+        process_step(
+            ctx.borrow(),
+            &CheckedProofStep::DeleteRatClause {
+                id,
+                keep_as_redundant: false,
+                clause: &clause[..],
+                pivot: clause[0],
+                propagations: &ResolutionPropagations {},
+            },
+        )?;
+        ctx.part_mut(ClausesP).unit_clauses[var.index()] = None;
+    }
+
+    ctx.part_mut(VariablesP).var_data[var.index()] = VarData::default();
+
+    Ok(())
+}
+
+/// Check a ChangeSamplingMode step
+fn check_change_sampling_mode<'a>(
+    mut ctx: partial!(
+        Context<'a>,
+        mut ClausesP,
+        mut ProcessingP<'a>,
+        mut VariablesP,
+        CheckerStateP,
+    ),
+    var: Var,
+    sample: bool,
+) -> Result<(), CheckerError> {
+    ensure_var(ctx.borrow(), var);
+    let mut ctx_in = ctx;
+    let (variables, ctx) = ctx_in.split_part_mut(VariablesP);
+    let var_data = &mut variables.var_data[var.index()];
+    let sampling_mode = if sample {
+        SamplingMode::Sample
+    } else {
+        SamplingMode::Witness
+    };
+
+    if var_data.sampling_mode != sampling_mode {
+        var_data.sampling_mode = sampling_mode;
+
+        if let Some(user_var) = var_data.user_var {
+            let sampling_mode = if var_data.sampling_mode == SamplingMode::Witness {
+                CheckedSamplingMode::Witness
+            } else {
+                CheckedSamplingMode::Sample
+            };
+            process_step(
+                ctx_in.borrow(),
+                &CheckedProofStep::UserVar {
+                    var,
+                    user_var: Some(CheckedUserVar {
+                        user_var,
+                        sampling_mode,
+                        new_var: false,
+                    }),
+                },
+            )?;
+        } else if sampling_mode == SamplingMode::Sample {
+            return Err(CheckerError::check_failed(
+                ctx.part(CheckerStateP).step,
+                format!("cannot sample hidden variable {:?}", var),
+            ));
+        }
+    }
+
+    Ok(())
+}
+
+/// Check an AtClause step
+fn check_at_clause_step<'a>(
+    mut ctx: partial!(
+        Context<'a>,
+        mut CheckerStateP,
+        mut ClauseHasherP,
+        mut ClausesP,
+        mut ProcessingP<'a>,
+        mut RupCheckP,
+        mut TmpDataP,
+        mut VariablesP,
+    ),
+    redundant: bool,
+    clause: &[Lit],
+    propagation_hashes: &[ClauseHash],
+) -> Result<(), CheckerError> {
+    let mut tmp = replace(&mut ctx.part_mut(TmpDataP).tmp, vec![]);
+
+    if copy_canonical(&mut tmp, clause) {
+        return Err(CheckerError::check_failed(
+            ctx.part(CheckerStateP).step,
+            format!("clause {:?} is a tautology", tmp),
+        ));
+    }
+
+    check_clause_with_hashes(ctx.borrow(), &tmp, &*propagation_hashes)?;
+
+    let (id, added) = store_clause(ctx.borrow(), &tmp, redundant);
+
+    if !redundant {
+        let state = ctx.part_mut(CheckerStateP);
+        state.previous_irred_clause_id = Some(id);
+        state.previous_irred_clause_lits.clear();
+        state.previous_irred_clause_lits.extend_from_slice(&tmp);
+    }
+
+    match added {
+        StoreClauseResult::New => {
+            let (rup_check, mut ctx) = ctx.split_part(RupCheckP);
+            process_step(
+                ctx.borrow(),
+                &CheckedProofStep::AtClause {
+                    id,
+                    redundant,
+                    clause: &tmp,
+                    propagations: &rup_check.trace_ids,
+                },
+            )?;
+        }
+        StoreClauseResult::NewlyIrredundant => {
+            process_step(
+                ctx.borrow(),
+                &CheckedProofStep::MakeIrredundant { id, clause: &tmp },
+            )?;
+        }
+        StoreClauseResult::Duplicate => (),
+    }
+
+    ctx.part_mut(TmpDataP).tmp = tmp;
+
+    Ok(())
+}
+
+/// Check a DeleteClause step
+fn check_delete_clause_step<'a>(
+    mut ctx: partial!(
+        Context<'a>,
+        mut CheckerStateP,
+        mut ClausesP,
+        mut ProcessingP<'a>,
+        mut TmpDataP,
+        mut VariablesP,
+        ClauseHasherP,
+    ),
+    clause: &[Lit],
+    proof: DeleteClauseProof,
+) -> Result<(), CheckerError> {
+    let mut tmp = replace(&mut ctx.part_mut(TmpDataP).tmp, vec![]);
+
+    if copy_canonical(&mut tmp, clause) {
+        return Err(CheckerError::check_failed(
+            ctx.part(CheckerStateP).step,
+            format!("clause {:?} is a tautology", tmp),
+        ));
+    }
+
+    let redundant = proof == DeleteClauseProof::Redundant;
+
+    let mut subsumed_by = None;
+
+    match proof {
+        DeleteClauseProof::Redundant => (),
+        DeleteClauseProof::Satisfied => {
+            let is_subsumed = tmp.iter().any(|&lit| {
+                if let Some((
+                    true,
+                    UnitClause {
+                        id: UnitId::Global(id),
+                        ..
+                    },
+                )) = ctx.part(ClausesP).lit_value(lit)
+                {
+                    subsumed_by = Some(id);
+                    true
+                } else {
+                    false
+                }
+            });
+            if !is_subsumed {
+                return Err(CheckerError::check_failed(
+                    ctx.part(CheckerStateP).step,
+                    format!("deleted clause {:?} is not satisfied", clause),
+                ));
+            }
+        }
+        DeleteClauseProof::Simplified => {
+            subsumed_by = ctx.part(CheckerStateP).previous_irred_clause_id;
+            if !ctx
+                .part(CheckerStateP)
+                .subsumed_by_previous_irred_clause(&tmp)
+            {
+                return Err(CheckerError::check_failed(
+                    ctx.part(CheckerStateP).step,
+                    format!(
+                        "deleted clause {:?} is not subsumed by previous clause {:?}",
+                        clause,
+                        ctx.part(CheckerStateP).previous_irred_clause_lits
+                    ),
+                ));
+            }
+        }
+    }
+
+    ctx.part_mut(CheckerStateP).previous_irred_clause_id = None;
+    ctx.part_mut(CheckerStateP)
+        .previous_irred_clause_lits
+        .clear();
+
+    let (id, deleted) = delete_clause(ctx.borrow(), &tmp, redundant)?;
+
+    if redundant {
+        match deleted {
+            DeleteClauseResult::Removed => {
+                process_step(
+                    ctx.borrow(),
+                    &CheckedProofStep::DeleteClause { id, clause: &tmp },
+                )?;
+            }
+            DeleteClauseResult::Unchanged => (),
+            DeleteClauseResult::NewlyRedundant => unreachable!(),
+        }
+    } else {
+        match deleted {
+            DeleteClauseResult::Removed | DeleteClauseResult::NewlyRedundant => {
+                process_step(
+                    ctx.borrow(),
+                    &CheckedProofStep::DeleteAtClause {
+                        id,
+                        keep_as_redundant: deleted == DeleteClauseResult::NewlyRedundant,
+                        clause: &tmp,
+                        propagations: &[subsumed_by.unwrap()],
+                    },
+                )?;
+            }
+            DeleteClauseResult::Unchanged => (),
+        }
+    }
+
+    ctx.part_mut(TmpDataP).tmp = tmp;
+    Ok(())
+}
+
+/// Check a UnitClauses step
+fn check_unit_clauses_step<'a>(
+    mut ctx: partial!(
+        Context<'a>,
+        mut CheckerStateP,
+        mut ClauseHasherP,
+        mut ClausesP,
+        mut ProcessingP<'a>,
+        mut RupCheckP,
+        mut VariablesP,
+    ),
+    units: &[(Lit, ClauseHash)],
+) -> Result<(), CheckerError> {
+    for &(lit, hash) in units.iter() {
+        ensure_var(ctx.borrow(), lit.var());
+
+        let clause = [lit];
+        let propagation_hashes = [hash];
+        check_clause_with_hashes(ctx.borrow(), &clause[..], &propagation_hashes[..])?;
+
+        let (id, added) = store_unit_clause(ctx.borrow(), lit);
+
+        match added {
+            StoreClauseResult::New => {
+                let (rup_check, mut ctx) = ctx.split_part(RupCheckP);
+                process_step(
+                    ctx.borrow(),
+                    &CheckedProofStep::AtClause {
+                        id,
+                        redundant: false,
+                        clause: &clause,
+                        propagations: &rup_check.trace_ids,
+                    },
+                )?;
+            }
+            StoreClauseResult::Duplicate => (),
+            StoreClauseResult::NewlyIrredundant => unreachable!(),
+        }
+    }
+    Ok(())
+}
+
+/// Check a Model step
+fn check_model_step<'a>(
+    mut ctx: partial!(Context<'a>, mut ProcessingP<'a>, CheckerStateP, ClausesP, VariablesP),
+    model: &[Lit],
+) -> Result<(), CheckerError> {
+    let mut assignments = HashSet::default();
+
+    for &lit in model.iter() {
+        if let Some((false, _)) = ctx.part(ClausesP).lit_value(lit) {
+            return Err(CheckerError::check_failed(
+                ctx.part(CheckerStateP).step,
+                format!("model assignment conflicts with unit clause {:?}", !lit),
+            ));
+        }
+        if assignments.contains(&!lit) {
+            return Err(CheckerError::check_failed(
+                ctx.part(CheckerStateP).step,
+                format!("model contains conflicting assignment {:?}", !lit),
+            ));
+        }
+        assignments.insert(lit);
+    }
+
+    for &lit in ctx.part(CheckerStateP).assumptions.iter() {
+        if !assignments.contains(&lit) {
+            return Err(CheckerError::check_failed(
+                ctx.part(CheckerStateP).step,
+                format!("model does not contain assumption {:?}", lit),
+            ));
+        }
+    }
+
+    for (_, candidates) in ctx.part(ClausesP).clauses.iter() {
+        for clause in candidates.iter() {
+            let lits = clause.lits.slice(&ctx.part(ClausesP).literal_buffer);
+            if !lits.iter().any(|lit| assignments.contains(&lit)) {
+                return Err(CheckerError::check_failed(
+                    ctx.part(CheckerStateP).step,
+                    format!("model does not satisfy clause {:?}", lits),
+                ));
+            }
+        }
+    }
+
+    process_step(ctx.borrow(), &CheckedProofStep::Model { assignment: model })?;
+
+    Ok(())
+}
+
+/// Check a FailedAssumptions step
+fn check_failed_assumptions_step<'a>(
+    mut ctx: partial!(
+        Context<'a>,
+        mut ClauseHasherP,
+        mut ClausesP,
+        mut ProcessingP<'a>,
+        mut RupCheckP,
+        mut TmpDataP,
+        mut VariablesP,
+        CheckerStateP,
+    ),
+    failed_core: &[Lit],
+    propagation_hashes: &[ClauseHash],
+) -> Result<(), CheckerError> {
+    let mut tmp = replace(&mut ctx.part_mut(TmpDataP).tmp, vec![]);
+
+    let direct_conflict = copy_canonical(&mut tmp, failed_core);
+
+    if !is_subset(&tmp, &ctx.part(CheckerStateP).assumptions, false) {
+        return Err(CheckerError::check_failed(
+            ctx.part(CheckerStateP).step,
+            "failed core contains non-assumed variables".to_string(),
+        ));
+    }
+
+    if direct_conflict {
+        // we have x and not x among the assumptions, no need to check
+        ctx.part_mut(RupCheckP).trace_ids.clear();
+    } else {
+        // invert the assumptions and check for an AT
+        for lit in tmp.iter_mut() {
+            *lit = !*lit;
+        }
+        check_clause_with_hashes(ctx.borrow(), &tmp, propagation_hashes)?;
+
+        // we undo the inversion to report the correct checked proof step
+        for lit in tmp.iter_mut() {
+            *lit = !*lit;
+        }
+    }
+
+    let (rup_check, mut ctx) = ctx.split_part(RupCheckP);
+    process_step(
+        ctx.borrow(),
+        &CheckedProofStep::FailedAssumptions {
+            failed_core: &tmp,
+            propagations: &rup_check.trace_ids,
+        },
+    )?;
+
+    ctx.part_mut(TmpDataP).tmp = tmp;
+
+    Ok(())
+}
+
+/// Checks a proof in the native Varisat format.
+pub fn check_proof<'a>(
+    mut ctx: partial!(
+        Context<'a>,
+        mut CheckerStateP,
+        mut ClauseHasherP,
+        mut ClausesP,
+        mut ProcessingP<'a>,
+        mut RupCheckP,
+        mut TmpDataP,
+        mut VariablesP,
+    ),
+    input: impl io::Read,
+) -> Result<(), CheckerError> {
+    let mut buffer = io::BufReader::new(input);
+    let mut parser = Parser::default();
+
+    while !ctx.part(CheckerStateP).ended {
+        ctx.part_mut(CheckerStateP).step += 1;
+
+        let step = ctx.part(CheckerStateP).step;
+
+        if step % 100000 == 0 {
+            log::info!("checking step {}k", step / 1000);
+        }
+
+        match parser.parse_step(&mut buffer) {
+            Ok(step) => check_step(ctx.borrow(), step)?,
+            Err(err) => match err.downcast::<io::Error>() {
+                Ok(io_err) => {
+                    if io_err.kind() == io::ErrorKind::UnexpectedEof {
+                        return Err(CheckerError::ProofIncomplete { step });
+                    } else {
+                        return Err(CheckerError::IoError {
+                            step,
+                            cause: io_err,
+                        });
+                    }
+                }
+                Err(err) => return Err(CheckerError::ParseError { step, cause: err }),
+            },
+        }
+    }
+
+    process_unit_conflicts(ctx.borrow())
+}
+
+/// Process unit conflicts detected during clause loading.
+pub fn process_unit_conflicts<'a>(
+    mut ctx: partial!(Context<'a>, mut ProcessingP<'a>, ClausesP, VariablesP),
+) -> Result<(), CheckerError> {
+    let (clauses, mut ctx) = ctx.split_part(ClausesP);
+    if let Some(ids) = &clauses.unit_conflict {
+        let clause = &[];
+
+        process_step(
+            ctx.borrow(),
+            &CheckedProofStep::AtClause {
+                id: clauses.next_clause_id,
+                redundant: false,
+                clause,
+                propagations: ids,
+            },
+        )?;
+    }
+
+    Ok(())
+}
diff --git a/vendor/varisat-checker/src/tmp.rs b/vendor/varisat-checker/src/tmp.rs
new file mode 100644
index 000000000..2c144218f
--- /dev/null
+++ b/vendor/varisat-checker/src/tmp.rs
@@ -0,0 +1,8 @@
+//! Temporary data.
+use varisat_formula::Lit;
+
+#[derive(Default)]
+pub struct TmpData {
+    /// Temporary storage for literals.
+    pub tmp: Vec<Lit>,
+}
diff --git a/vendor/varisat-checker/src/transcript.rs b/vendor/varisat-checker/src/transcript.rs
new file mode 100644
index 000000000..c96829ea5
--- /dev/null
+++ b/vendor/varisat-checker/src/transcript.rs
@@ -0,0 +1,133 @@
+//! Proof transcripts.
+use anyhow::Error;
+
+use varisat_formula::{Lit, Var};
+
+use crate::processing::{CheckedProofStep, CheckedSamplingMode, CheckedUserVar, CheckerData};
+
+/// Step of a proof transcript.
+///
+/// The proof transcript contains the solver queries and results that correspond to a checked proof.
+///
+/// The transcript uses the same variable numbering as used for solver calls.
+#[derive(Debug)]
+pub enum ProofTranscriptStep<'a> {
+    WitnessVar { var: Var },
+    SampleVar { var: Var },
+    HideVar { var: Var },
+    ObserveInternalVar { var: Var },
+    AddClause { clause: &'a [Lit] },
+    Unsat,
+    Model { assignment: &'a [Lit] },
+    Assume { assumptions: &'a [Lit] },
+    FailedAssumptions { failed_core: &'a [Lit] },
+}
+
+/// Implement to process transcript steps.
+pub trait ProofTranscriptProcessor {
+    /// Process a single proof transcript step.
+    fn process_step(&mut self, step: &ProofTranscriptStep) -> Result<(), Error>;
+}
+
+/// Create a transcript from proof steps
+#[derive(Default)]
+pub(crate) struct Transcript {
+    lit_buf: Vec<Lit>,
+}
+
+impl Transcript {
+    /// If a checked proof step has a corresponding transcript step, return that.
+    pub fn transcript_step(
+        &mut self,
+        step: &CheckedProofStep,
+        data: CheckerData,
+    ) -> Option<ProofTranscriptStep> {
+        match step {
+            CheckedProofStep::UserVar { var, user_var } => match user_var {
+                None => Some(ProofTranscriptStep::HideVar {
+                    var: data.user_from_proof_var(*var).unwrap(),
+                }),
+
+                Some(CheckedUserVar {
+                    sampling_mode: CheckedSamplingMode::Sample,
+                    new_var: true,
+                    ..
+                }) => None,
+
+                Some(CheckedUserVar {
+                    user_var,
+                    sampling_mode: CheckedSamplingMode::Witness,
+                    new_var: true,
+                }) => Some(ProofTranscriptStep::ObserveInternalVar { var: *user_var }),
+
+                Some(CheckedUserVar {
+                    user_var,
+                    sampling_mode: CheckedSamplingMode::Witness,
+                    new_var: false,
+                }) => Some(ProofTranscriptStep::WitnessVar { var: *user_var }),
+
+                Some(CheckedUserVar {
+                    user_var,
+                    sampling_mode: CheckedSamplingMode::Sample,
+                    new_var: false,
+                }) => Some(ProofTranscriptStep::SampleVar { var: *user_var }),
+            },
+            CheckedProofStep::AddClause { clause, .. }
+            | CheckedProofStep::DuplicatedClause { clause, .. }
+            | CheckedProofStep::TautologicalClause { clause, .. } => {
+                self.lit_buf.clear();
+                self.lit_buf.extend(clause.iter().map(|&lit| {
+                    lit.map_var(|var| {
+                        data.user_from_proof_var(var)
+                            .expect("hidden variable in clause")
+                    })
+                }));
+                Some(ProofTranscriptStep::AddClause {
+                    clause: &self.lit_buf,
+                })
+            }
+            CheckedProofStep::AtClause { clause, .. } => {
+                if clause.is_empty() {
+                    Some(ProofTranscriptStep::Unsat)
+                } else {
+                    None
+                }
+            }
+            CheckedProofStep::Model { assignment } => {
+                self.lit_buf.clear();
+                self.lit_buf.extend(assignment.iter().flat_map(|&lit| {
+                    data.user_from_proof_var(lit.var())
+                        .map(|var| var.lit(lit.is_positive()))
+                }));
+                Some(ProofTranscriptStep::Model {
+                    assignment: &self.lit_buf,
+                })
+            }
+            CheckedProofStep::Assumptions { assumptions } => {
+                self.lit_buf.clear();
+                self.lit_buf.extend(assumptions.iter().map(|&lit| {
+                    lit.map_var(|var| {
+                        data.user_from_proof_var(var)
+                            .expect("hidden variable in assumptions")
+                    })
+                }));
+                Some(ProofTranscriptStep::Assume {
+                    assumptions: &self.lit_buf,
+                })
+            }
+            CheckedProofStep::FailedAssumptions { failed_core, .. } => {
+                self.lit_buf.clear();
+                self.lit_buf.extend(failed_core.iter().map(|&lit| {
+                    lit.map_var(|var| {
+                        data.user_from_proof_var(var)
+                            .expect("hidden variable in assumptions")
+                    })
+                }));
+                Some(ProofTranscriptStep::FailedAssumptions {
+                    failed_core: &self.lit_buf,
+                })
+            }
+            _ => None,
+        }
+    }
+}
diff --git a/vendor/varisat-checker/src/variables.rs b/vendor/varisat-checker/src/variables.rs
new file mode 100644
index 000000000..51adb1b98
--- /dev/null
+++ b/vendor/varisat-checker/src/variables.rs
@@ -0,0 +1,195 @@
+//! Variable metadata.
+use partial_ref::{partial, PartialRef};
+use rustc_hash::FxHashSet as HashSet;
+
+use varisat_formula::Var;
+
+use crate::{
+    context::{parts::*, Context},
+    processing::{process_step, CheckedProofStep, CheckedSamplingMode, CheckedUserVar},
+    CheckerError,
+};
+
+/// Data for each literal.
+#[derive(Clone, Default)]
+pub struct LitData {
+    pub clause_count: usize,
+}
+
+#[derive(Copy, Clone, PartialEq, Eq)]
+pub enum SamplingMode {
+    Sample,
+    Witness,
+    Hide,
+}
+
+/// Data for each variable.
+#[derive(Clone)]
+pub struct VarData {
+    pub user_var: Option<Var>,
+    pub sampling_mode: SamplingMode,
+}
+
+impl Default for VarData {
+    fn default() -> VarData {
+        VarData {
+            user_var: None,
+            sampling_mode: SamplingMode::Sample,
+        }
+    }
+}
+
+#[derive(Default)]
+pub struct Variables {
+    /// Information about literals in the current formula.
+    pub lit_data: Vec<LitData>,
+    /// Information about variables in the current formula.
+    pub var_data: Vec<VarData>,
+    /// User var names in use.
+    ///
+    /// This is used to check for colliding mappings which are not allowed.
+    used_user_vars: HashSet<Var>,
+}
+
+/// Check that var is a sampling user var and create new variables as necessary.
+pub fn ensure_sampling_var(
+    mut ctx: partial!(Context, mut ClausesP, mut VariablesP, CheckerStateP),
+    var: Var,
+) -> Result<(), CheckerError> {
+    ensure_var(ctx.borrow(), var);
+
+    let variables = ctx.part_mut(VariablesP);
+
+    if variables.var_data[var.index()].sampling_mode != SamplingMode::Sample {
+        return Err(CheckerError::check_failed(
+            ctx.part(CheckerStateP).step,
+            format!("variable {:?} is not a sampling variable", var),
+        ));
+    }
+    Ok(())
+}
+
+/// Ensure that a variable is present.
+pub fn ensure_var(mut ctx: partial!(Context, mut ClausesP, mut VariablesP), var: Var) {
+    let (variables, mut ctx) = ctx.split_part_mut(VariablesP);
+
+    if variables.var_data.len() <= var.index() {
+        variables
+            .var_data
+            .resize(var.index() + 1, VarData::default());
+        variables
+            .lit_data
+            .resize((var.index() + 1) * 2, LitData::default());
+        ctx.part_mut(ClausesP)
+            .unit_clauses
+            .resize(var.index() + 1, None);
+    }
+}
+
+/// Add a user/global var mapping.
+pub fn add_user_mapping<'a>(
+    mut ctx: partial!(Context<'a>, mut ClausesP, mut ProcessingP<'a>, mut VariablesP, CheckerStateP),
+    global_var: Var,
+    user_var: Var,
+) -> Result<(), CheckerError> {
+    ensure_var(ctx.borrow(), global_var);
+
+    let mut ctx_in = ctx;
+    let (variables, ctx) = ctx_in.split_part_mut(VariablesP);
+
+    // TODO will the first check cause problems when observing solver added variables?
+    // That check is required for the workaround in CheckerData's user from proof method
+    if user_var.index() >= variables.var_data.len() || variables.used_user_vars.contains(&user_var)
+    {
+        return Err(CheckerError::check_failed(
+            ctx.part(CheckerStateP).step,
+            format!("user name {:?} used for two different variables", user_var),
+        ));
+    }
+
+    let var_data = &mut variables.var_data[global_var.index()];
+
+    // sampling_mode will be Witness for a newly observed internal variable and Sample for a a
+    // fresh variable
+    if var_data.sampling_mode == SamplingMode::Hide {
+        return Err(CheckerError::check_failed(
+            ctx.part(CheckerStateP).step,
+            format!(
+                "user name added to variable {:?} which is still hidden",
+                global_var
+            ),
+        ));
+    }
+
+    if var_data.user_var.is_some() {
+        return Err(CheckerError::check_failed(
+            ctx.part(CheckerStateP).step,
+            format!("change of user name for in use varible {:?}", global_var),
+        ));
+    }
+
+    var_data.user_var = Some(user_var);
+
+    variables.used_user_vars.insert(user_var);
+
+    let sampling_mode = if var_data.sampling_mode == SamplingMode::Witness {
+        CheckedSamplingMode::Witness
+    } else {
+        CheckedSamplingMode::Sample
+    };
+
+    process_step(
+        ctx_in.borrow(),
+        &CheckedProofStep::UserVar {
+            var: global_var,
+            user_var: Some(CheckedUserVar {
+                user_var,
+                sampling_mode,
+                new_var: true,
+            }),
+        },
+    )?;
+
+    Ok(())
+}
+
+/// Remove a user/global var mapping.
+pub fn remove_user_mapping<'a>(
+    mut ctx: partial!(Context<'a>, mut ClausesP, mut ProcessingP<'a>, mut VariablesP, CheckerStateP),
+    global_var: Var,
+) -> Result<(), CheckerError> {
+    ensure_var(ctx.borrow(), global_var);
+
+    let variables = ctx.part_mut(VariablesP);
+
+    let var_data = &variables.var_data[global_var.index()];
+
+    // We process this step before removing the mapping, so the processor can still look up the
+    // mapping.
+
+    if var_data.user_var.is_some() {
+        process_step(
+            ctx.borrow(),
+            &CheckedProofStep::UserVar {
+                var: global_var,
+                user_var: None,
+            },
+        )?;
+    } else {
+        return Err(CheckerError::check_failed(
+            ctx.part(CheckerStateP).step,
+            format!("no user name to remove for variable {:?}", global_var),
+        ));
+    }
+
+    let variables = ctx.part_mut(VariablesP);
+
+    let var_data = &mut variables.var_data[global_var.index()];
+    if let Some(user_var) = var_data.user_var {
+        variables.used_user_vars.remove(&user_var);
+        var_data.user_var = None;
+        var_data.sampling_mode = SamplingMode::Hide;
+    }
+
+    Ok(())
+}