patronus 0.38.1

// Copyright 2024 Cornell University
// released under BSD 3-Clause License
// author: Kevin Laeufer <laeufer@cornell.edu>

use crate::expr::{Context, ExprRef};
use crate::smt::parser::{
    SmtParserError, count_parens, parse_get_unsat_assumptions_response, parse_get_value_response,
};
use crate::smt::serialize::serialize_cmd;
use rustc_hash::FxHashMap;
use std::fs::File;
use std::io::{BufRead, BufReader, BufWriter};
use std::io::{Read, Write};
use std::process::{Command, Stdio};
use thiserror::Error;

/// A SMT Solver Error.
#[derive(Error, Debug)]
pub enum Error {
    #[error("[smt] I/O operation failed")]
    Io(#[from] std::io::Error),
    #[error("[smt] cannot pop because the stack is already empty")]
    StackUnderflow,
    #[error("[smt] {0} reported an error:\n{1}")]
    FromSolver(String, String),
    #[error("[smt]{0} is unreachable, the process might have died")]
    SolverDead(String),
    #[error("[smt] {0} returned an unexpected response:\n{1}")]
    UnexpectedResponse(String, String),
    #[error("[smt] failed to parse a response")]
    Parser(#[from] SmtParserError),
}

pub type Result<T> = std::result::Result<T, Error>;
type SymbolTable = FxHashMap<String, ExprRef>;

/// An SMT Logic.
#[derive(Debug, Clone, Eq, PartialEq)]
pub enum Logic {
    All,
    QfAufbv,
    QfAbv,
    QfBv,
}

impl Logic {
    pub(crate) fn to_smt_str(&self) -> &'static str {
        match self {
            Logic::All => "ALL",
            Logic::QfAufbv => "QF_AUFBV",
            Logic::QfAbv => "QF_ABV",
            Logic::QfBv => "QF_BV",
        }
    }
}

/// A command to an SMT solver.
#[derive(Debug, Clone, Eq, PartialEq)]
pub enum SmtCommand {
    Exit,
    CheckSat,
    SetLogic(Logic),
    SetOption(String, String),
    SetInfo(String, String),
    Assert(ExprRef),
    DeclareConst(ExprRef),
    DefineConst(ExprRef, ExprRef),
    CheckSatAssuming(Vec<ExprRef>),
    Push(u64),
    Pop(u64),
    GetValue(ExprRef),
    GetUnsatAssumptions,
}

/// The result of a `(check-sat)` command.
#[derive(Debug, Clone, Eq, PartialEq)]
pub enum CheckSatResponse {
    Sat,
    Unsat,
    Unknown,
}

/// Represents the meta data of an SMT Solver
pub trait SolverMetaData {
    // properties
    fn name(&self) -> &str;
    fn supports_check_assuming(&self) -> bool;
    fn supports_uf(&self) -> bool;
    /// Indicates whether the solver supports the non-standard `(as const)` command.
    fn supports_const_array(&self) -> bool;
    fn supports_get_unsat_assumptions(&self) -> bool;
}

/// Allows an SMT solver to start a Context.
pub trait Solver: SolverMetaData {
    type Context: SolverContext;
    /// Launch a new instance of this solver.
    fn start(&self, replay_file: Option<File>) -> Result<Self::Context>;
}

/// Interface to a running SMT Solver with everything executing as blocking I/O.
pub trait SolverContext: SolverMetaData {
    // type Replay : Write + Send;
    fn restart(&mut self) -> Result<()>;
    fn set_logic(&mut self, option: Logic) -> Result<()>;
    fn assert(&mut self, ctx: &Context, e: ExprRef) -> Result<()>;
    fn declare_const(&mut self, ctx: &Context, symbol: ExprRef) -> Result<()>;
    fn define_const(&mut self, ctx: &Context, symbol: ExprRef, expr: ExprRef) -> Result<()>;
    fn check_sat_assuming(
        &mut self,
        ctx: &Context,
        props: impl IntoIterator<Item = ExprRef>,
    ) -> Result<CheckSatResponse>;
    fn check_sat(&mut self) -> Result<CheckSatResponse>;
    fn push(&mut self) -> Result<()>;
    fn pop(&mut self) -> Result<()>;
    fn get_value(&mut self, ctx: &mut Context, e: ExprRef) -> Result<ExprRef>;

    /// # Preconditions
    /// * Must have preceding `UNSAT` query, else behavior is undefined
    fn get_unsat_assumptions(&mut self, ctx: &mut Context) -> Result<Vec<ExprRef>>;
}

#[derive(Debug, Clone, Eq, PartialEq)]
pub struct SmtLibSolver {
    name: &'static str,
    args: &'static [&'static str],
    options: &'static [&'static str],
    supports_uf: bool,
    supports_check_assuming: bool,
    supports_const_array: bool,
    supports_unsat_assumptions: bool,
}

impl SolverMetaData for SmtLibSolver {
    fn name(&self) -> &str {
        self.name
    }

    fn supports_check_assuming(&self) -> bool {
        self.supports_check_assuming
    }

    fn supports_uf(&self) -> bool {
        self.supports_uf
    }

    fn supports_const_array(&self) -> bool {
        self.supports_const_array
    }

    fn supports_get_unsat_assumptions(&self) -> bool {
        self.supports_unsat_assumptions
    }
}

impl Solver for SmtLibSolver {
    type Context = SmtLibSolverCtx;
    fn start(&self, replay_file: Option<File>) -> Result<Self::Context> {
        let mut proc = Command::new(self.name)
            .args(self.args)
            .stdin(Stdio::piped())
            .stdout(Stdio::piped())
            .stderr(Stdio::piped())
            .spawn()?;
        let stdin = BufWriter::new(proc.stdin.take().unwrap());
        let stdout = BufReader::new(proc.stdout.take().unwrap());
        let stderr = proc.stderr.take().unwrap();
        let mut solver = SmtLibSolverCtx {
            name: self.name.to_string(),
            proc,
            stdin,
            stdout,
            stderr,
            stack_depth: 0,
            response: String::new(),
            replay_file: replay_file.map(BufWriter::new),
            has_error: false,
            solver_args: self.args.iter().map(|a| a.to_string()).collect(),
            solver_options: self.options.iter().map(|a| a.to_string()).collect(),
            supports_uf: self.supports_uf,
            supports_check_assuming: self.supports_check_assuming,
            supports_const_array: self.supports_const_array,
            supports_get_unsat_assumptions: self.supports_unsat_assumptions,
            symbols: vec![SymbolTable::default()],
            last_query_unsat: false,
        };
        for option in self.options.iter() {
            solver.write_cmd(
                None,
                &SmtCommand::SetOption(option.to_string(), "true".to_string()),
            )?
        }
        Ok(solver)
    }
}

/// Launches an SMT solver and communicates through `stdin` using SMTLib commands.
pub struct SmtLibSolverCtx {
    name: String,
    proc: std::process::Child,
    stdin: BufWriter<std::process::ChildStdin>,
    stdout: BufReader<std::process::ChildStdout>,
    stderr: std::process::ChildStderr,
    stack_depth: usize,
    response: String,
    replay_file: Option<BufWriter<File>>,
    /// keeps track of whether there was an error from the solver which might make regular shutdown
    /// impossible
    has_error: bool,
    // metadata to be able to restart solver
    solver_args: Vec<String>,
    solver_options: Vec<String>,
    // solver capabilities
    supports_uf: bool,
    supports_check_assuming: bool,
    supports_const_array: bool,
    supports_get_unsat_assumptions: bool,
    /// Internal symbol tables for each solver context
    /// **Representation invariant**: `symbols.len() > 0`
    symbols: Vec<SymbolTable>,
    /// Flag for whether last query was `UNSAT`
    last_query_unsat: bool,
}

impl SmtLibSolverCtx {
    #[inline]
    fn write_cmd(&mut self, ctx: Option<&Context>, cmd: &SmtCommand) -> Result<()> {
        if let Some(rf) = self.replay_file.as_mut() {
            serialize_cmd(rf, ctx, cmd)?;
        }
        serialize_cmd(&mut self.stdin, ctx, cmd)?;
        if let Some(rf) = self.replay_file.as_mut() {
            rf.flush()?;
        }
        match self.stdin.flush() {
            Err(e) if e.kind() == std::io::ErrorKind::BrokenPipe => {
                // make sure we drop the replay file
                let _ = self.replay_file.take();
                // check to see if we can find an error message
                match self.read_response() {
                    Err(e @ Error::FromSolver(_, _)) => Err(e),
                    _ => Err(Error::SolverDead(self.name.clone())),
                }
            }
            Err(other) => Err(other.into()),
            Ok(_) => Ok(()),
        }
    }

    /// after this function executes, the result will be available in `self.result`.
    fn read_response(&mut self) -> Result<()> {
        self.response.clear();
        // our basic assumptions are:
        // 1. the solver will terminate its answer with '\n'
        // 2. the answer will contain a balanced number of parenthesis
        self.stdout.read_line(&mut self.response)?;
        while count_parens(&self.response) > 0 {
            self.response.push(' ');
            self.stdout.read_line(&mut self.response)?;
        }

        // check to see if there was an error reported on stdout
        if self.response.trim_start().starts_with("(error") {
            let trimmed = self.response.trim();
            let start = "(error ".len();
            let msg = &trimmed[start..(trimmed.len() - start - 1)];
            self.has_error = true;
            Err(Error::FromSolver(self.name.clone(), msg.to_string()))
        } else {
            // check if the process is still alive
            match self.proc.try_wait() {
                Ok(Some(status)) if !status.success() => {
                    // solver terminated with error return code
                    // check for output on stderror
                    let mut err = vec![];
                    self.stderr.read_to_end(&mut err)?;
                    self.has_error = true;
                    Err(Error::FromSolver(
                        self.name.clone(),
                        String::from_utf8_lossy(&err).to_string(),
                    ))
                }
                _ => Ok(()),
            }
        }
    }

    fn read_sat_response(&mut self) -> Result<CheckSatResponse> {
        self.stdin.flush()?; // make sure that the commands reached the solver
        self.read_response()?;
        let response = self.response.trim();
        match response {
            "sat" => Ok(CheckSatResponse::Sat),
            "unsat" => Ok(CheckSatResponse::Unsat),
            other => Err(Error::UnexpectedResponse(
                self.name.clone(),
                other.to_string(),
            )),
        }
    }
}

impl Drop for SmtLibSolverCtx {
    fn drop(&mut self) {
        shut_down_solver(self);
    }
}

/// internal method to try to cleanly shut down the solver process
fn shut_down_solver(solver: &mut SmtLibSolverCtx) {
    // try to close the child process as not to leak resources
    if solver.write_cmd(None, &SmtCommand::Exit).is_ok() {
        let _status = solver
            .proc
            .wait()
            .expect("failed to wait for SMT solver to exit");
    }
    // we don't care whether the solver crashed or returned success, as long as it is cleaned up
}

impl SolverMetaData for SmtLibSolverCtx {
    fn name(&self) -> &str {
        &self.name
    }

    fn supports_uf(&self) -> bool {
        self.supports_uf
    }
    fn supports_check_assuming(&self) -> bool {
        self.supports_check_assuming
    }

    fn supports_const_array(&self) -> bool {
        self.supports_const_array
    }

    fn supports_get_unsat_assumptions(&self) -> bool {
        self.supports_get_unsat_assumptions
    }
}

impl SolverContext for SmtLibSolverCtx {
    fn restart(&mut self) -> Result<()> {
        shut_down_solver(self);

        let mut proc = Command::new(&self.name)
            .args(&self.solver_args)
            .stdin(Stdio::piped())
            .stdout(Stdio::piped())
            .stderr(Stdio::piped())
            .spawn()?;
        let stdin = BufWriter::new(proc.stdin.take().unwrap());
        let stdout = BufReader::new(proc.stdout.take().unwrap());
        let stderr = proc.stderr.take().unwrap();
        self.proc = proc;
        self.stdin = stdin;
        self.stdout = stdout;
        self.stderr = stderr;
        for option in self.solver_options.clone() {
            self.write_cmd(None, &SmtCommand::SetOption(option, "true".to_string()))?;
        }
        self.symbols = vec![SymbolTable::default()];
        self.last_query_unsat = false;
        Ok(())
    }

    fn set_logic(&mut self, logic: Logic) -> Result<()> {
        self.write_cmd(None, &SmtCommand::SetLogic(logic))
    }

    fn assert(&mut self, ctx: &Context, e: ExprRef) -> Result<()> {
        self.write_cmd(Some(ctx), &SmtCommand::Assert(e))
    }

    fn declare_const(&mut self, ctx: &Context, symbol: ExprRef) -> Result<()> {
        // Add new constant into current context's symbol table
        self.symbols
            .last_mut()
            .unwrap()
            .insert(ctx.get_symbol_name(symbol).unwrap().to_string(), symbol);
        self.write_cmd(Some(ctx), &SmtCommand::DeclareConst(symbol))
    }

    fn define_const(&mut self, ctx: &Context, symbol: ExprRef, expr: ExprRef) -> Result<()> {
        // Add new constant into current context's symbol table
        self.symbols
            .last_mut()
            .unwrap()
            .insert(ctx.get_symbol_name(symbol).unwrap().to_string(), symbol);
        self.write_cmd(Some(ctx), &SmtCommand::DefineConst(symbol, expr))
    }

    fn check_sat_assuming(
        &mut self,
        ctx: &Context,
        props: impl IntoIterator<Item = ExprRef>,
    ) -> Result<CheckSatResponse> {
        let props: Vec<ExprRef> = props.into_iter().collect();
        self.write_cmd(Some(ctx), &SmtCommand::CheckSatAssuming(props))?;
        let res = self.read_sat_response()?;
        self.last_query_unsat = matches!(res, CheckSatResponse::Unsat);
        Ok(res)
    }

    fn check_sat(&mut self) -> Result<CheckSatResponse> {
        self.write_cmd(None, &SmtCommand::CheckSat)?;
        let res = self.read_sat_response()?;
        self.last_query_unsat = matches!(res, CheckSatResponse::Unsat);
        Ok(res)
    }

    fn push(&mut self) -> Result<()> {
        self.write_cmd(None, &SmtCommand::Push(1))?;
        // Add new symbol table for context
        self.symbols.push(SymbolTable::default());
        self.stack_depth += 1;
        Ok(())
    }

    fn pop(&mut self) -> Result<()> {
        if self.stack_depth > 0 {
            self.write_cmd(None, &SmtCommand::Pop(1))?;
            // Remove symbol table from old context
            self.symbols.pop();
            self.stack_depth -= 1;
            Ok(())
        } else {
            Err(Error::StackUnderflow)
        }
    }

    fn get_value(&mut self, ctx: &mut Context, e: ExprRef) -> Result<ExprRef> {
        self.write_cmd(Some(ctx), &SmtCommand::GetValue(e))?;
        self.stdin.flush()?; // make sure that the commands reached the solver
        self.read_response()?;
        let response = self.response.trim();
        let expr = parse_get_value_response(ctx, response.as_bytes())?;
        Ok(expr)
    }

    fn get_unsat_assumptions(&mut self, ctx: &mut Context) -> Result<Vec<ExprRef>> {
        if !self.last_query_unsat {
            return Err(Error::FromSolver(
                self.name.clone(),
                "Previous query not UNSAT".into(),
            ));
        }

        // Stage `(get-unsat-assumptions)` command
        self.write_cmd(None, &SmtCommand::GetUnsatAssumptions)?;
        self.stdin.flush()?;
        self.read_response()?;
        let response = self.response.trim();

        let mut st = SymbolTable::default();
        for st_ctx in &self.symbols {
            st.extend(st_ctx.iter().map(|(k, &v)| (k.clone(), v)));
        }

        Ok(parse_get_unsat_assumptions_response(
            ctx,
            &st,
            response.as_bytes(),
        )?)
    }
}

pub const BITWUZLA: SmtLibSolver = SmtLibSolver {
    name: "bitwuzla",
    args: &[],
    options: &["incremental", "produce-models", "produce-unsat-assumptions"],
    supports_uf: false,
    supports_check_assuming: true,
    supports_const_array: true,
    supports_unsat_assumptions: true,
};

pub const YICES2: SmtLibSolver = SmtLibSolver {
    name: "yices-smt2",
    args: &["--incremental"],
    options: &[],
    supports_uf: false, // actually true, but ignoring for now
    supports_check_assuming: false,
    // see https://github.com/SRI-CSL/yices2/issues/110
    supports_const_array: false,
    supports_unsat_assumptions: false,
};

pub const Z3: SmtLibSolver = SmtLibSolver {
    name: "z3",
    args: &["-in"],
    options: &["produce-unsat-assumptions"],
    supports_uf: true,
    supports_check_assuming: true,
    supports_const_array: true,
    supports_unsat_assumptions: true,
};

pub const CVC5: SmtLibSolver = SmtLibSolver {
    name: "cvc5",
    args: &["--incremental", "--produce-models"],
    options: &["produce-unsat-assumptions"],
    supports_uf: true,
    supports_check_assuming: true,
    supports_const_array: true,
    supports_unsat_assumptions: true,
};

/// Name of the environment variable used by the test suite to select which SMT
/// solver to run against. See [`solver_from_env`].
pub const TEST_SOLVER_ENV: &str = "PATRONUS_TEST_SOLVER";

/// Returns the SMT solver selected by the `PATRONUS_TEST_SOLVER` environment
/// variable, defaulting to [`BITWUZLA`] when the variable is unset or empty.
///
/// Recognized values are `bitwuzla`, `yices2`, `cvc5` and `z3`. This lets the
/// test suite run against every solver configured in CI by setting a single
/// environment variable per matrix entry. Panics on an unrecognized value so a
/// typo in the CI configuration fails loudly instead of silently falling back.
pub fn solver_from_env() -> SmtLibSolver {
    match std::env::var(TEST_SOLVER_ENV).ok().as_deref() {
        None | Some("" | "bitwuzla") => BITWUZLA,
        Some("yices2") => YICES2,
        Some("cvc5") => CVC5,
        Some("z3") => Z3,
        Some(other) => panic!(
            "unrecognized {TEST_SOLVER_ENV}={other:?}; expected one of: bitwuzla, yices2, cvc5, z3"
        ),
    }
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn test_error() {
        let mut ctx = Context::default();
        let mut solver = solver_from_env().start(None).unwrap();
        solver.set_logic(Logic::QfBv).unwrap();
        let a = ctx.bv_symbol("a", 3);
        let e = ctx.build(|c| c.equal(a, c.bit_vec_val(3, 3)));
        solver.assert(&ctx, e).unwrap();
        let res = solver.check_sat();
        assert!(res.is_err(), "a was not declared!");
        // after this error, the solver is dead and won't respond!
        let _res = solver.declare_const(&ctx, a);
        // assert!(res.is_err());
        // TODO: this does not always work? do we need to wait longer?
    }

    #[test]
    fn test_check_sat_assuming() {
        let backend = solver_from_env();
        if !backend.supports_check_assuming() {
            return;
        }
        let mut ctx = Context::default();
        let a = ctx.bv_symbol("a", 3);
        let e = ctx.build(|c| c.equal(a, c.bit_vec_val(3, 3)));
        let mut solver = backend.start(None).unwrap();
        solver.set_logic(Logic::QfBv).unwrap();
        solver.declare_const(&ctx, a).unwrap();
        let res = solver.check_sat_assuming(&ctx, [e]);
        assert_eq!(res.unwrap(), CheckSatResponse::Sat);
        let value_of_a = solver.get_value(&mut ctx, a).unwrap();
        assert_eq!(value_of_a, ctx.bit_vec_val(3, 3));
    }

    /// Check that asserting `a == 3` and `a == 4` requires both facts to prove `UNSAT`
    #[test]
    fn test_unsat_assumptions_basic() {
        let backend = solver_from_env();
        if !backend.supports_get_unsat_assumptions() {
            return;
        }
        let mut ctx = Context::default();
        let a = ctx.bv_symbol("a", 3);
        let eq3 = ctx.build(|c| c.equal(a, c.bit_vec_val(3, 3)));
        let eq4 = ctx.build(|c| c.equal(a, c.bit_vec_val(4, 3)));

        let mut solver = backend.start(None).unwrap();
        solver.set_logic(Logic::QfBv).unwrap();
        solver.declare_const(&ctx, a).unwrap();

        let res = solver.check_sat_assuming(&ctx, [eq3, eq4]).unwrap();
        assert_eq!(res, CheckSatResponse::Unsat);

        let core = solver.get_unsat_assumptions(&mut ctx).unwrap();
        assert_eq!(core.len(), 2);
        assert!(core.contains(&eq3));
        assert!(core.contains(&eq4));
    }

    /// Check that asserting `false` initially is enough to prove `UNSAT`
    #[test]
    fn test_unsat_assumptions_false() {
        let backend = solver_from_env();
        if !backend.supports_get_unsat_assumptions() {
            return;
        }
        let mut ctx = Context::default();
        let smt_false = ctx.get_false();
        let a = ctx.bv_symbol("a", 3);
        let ge3 = ctx.build(|c| c.greater_or_equal(a, c.bit_vec_val(3, 3)));
        let ge5 = ctx.build(|c| c.greater_or_equal(a, c.bit_vec_val(5, 3)));

        let mut solver = backend.start(None).unwrap();
        solver.set_logic(Logic::QfBv).unwrap();
        solver.declare_const(&ctx, a).unwrap();
        let res = solver
            .check_sat_assuming(&ctx, [smt_false, ge3, ge5])
            .unwrap();
        assert_eq!(res, CheckSatResponse::Unsat);

        // `false` alone forces UNSAT and is therefore required. Cores are not
        // required to be minimal, so the redundant `ge3`/`ge5` may also appear.
        let core = solver.get_unsat_assumptions(&mut ctx).unwrap();
        assert!(core.contains(&smt_false));
    }

    /// Check that extra fact `b == 1` is not needed to prove `UNSAT` for `a == 3 /\ a == 4`
    #[test]
    fn test_unsat_assumptions_subset() {
        let backend = solver_from_env();
        if !backend.supports_get_unsat_assumptions() {
            return;
        }
        let mut ctx = Context::default();
        let a = ctx.bv_symbol("a", 3);
        let b = ctx.bv_symbol("b", 3);
        let eq3 = ctx.build(|c| c.equal(a, c.bit_vec_val(3, 3)));
        let eq4 = ctx.build(|c| c.equal(a, c.bit_vec_val(4, 3)));
        let b_is_1 = ctx.build(|c| c.equal(b, c.bit_vec_val(1, 3))); // unrelated, satisfiable

        let mut solver = backend.start(None).unwrap();
        solver.set_logic(Logic::QfBv).unwrap();
        solver.declare_const(&ctx, a).unwrap();
        solver.declare_const(&ctx, b).unwrap();

        let res = solver.check_sat_assuming(&ctx, [eq3, eq4, b_is_1]).unwrap();
        assert_eq!(res, CheckSatResponse::Unsat);

        // {eq3, eq4} is itself UNSAT, so any sufficient core must contain both.
        // Cores need not be minimal, so the unrelated `b_is_1` may also appear.
        let core = solver.get_unsat_assumptions(&mut ctx).unwrap();
        assert!(core.contains(&eq3) && core.contains(&eq4));
    }

    /// Simulate activation literal `UNSAT` assumptions by asserting
    /// `x == 2`, `x >= 5`, and `x >= 1` to yield `UNSAT` proof with only first two facts
    #[test]
    fn test_unsat_assumptions_act_lits() {
        let backend = solver_from_env();
        if !backend.supports_get_unsat_assumptions() {
            return;
        }
        let mut ctx = Context::default();
        let x = ctx.bv_symbol("x", 3);
        let eq2 = ctx.build(|c| c.equal(x, c.bit_vec_val(2, 3)));
        let ge5 = ctx.build(|c| c.greater_or_equal(x, c.bit_vec_val(5, 3)));
        let ge1 = ctx.build(|c| c.greater_or_equal(x, c.bit_vec_val(1, 3)));

        let mut solver = backend.start(None).unwrap();
        solver.set_logic(Logic::QfBv).unwrap();
        solver.declare_const(&ctx, x).unwrap();

        let mut act_lits = Vec::with_capacity(3);
        for (idx, expr) in [eq2, ge1, ge5].iter().enumerate() {
            let lit = ctx.bv_symbol(format!("a_{idx}").as_str(), 1);
            let imp = ctx.implies(lit, *expr);
            act_lits.push(lit);
            solver.declare_const(&ctx, lit).unwrap();
            solver.assert(&ctx, imp).unwrap();
        }

        let res = solver.check_sat_assuming(&ctx, act_lits.clone()).unwrap();
        assert_eq!(res, CheckSatResponse::Unsat);

        // act_lits[0] (x==2) and act_lits[2] (x>=5) are jointly UNSAT and thus
        // required. Cores need not be minimal, so the redundant act_lits[1] may appear.
        let core = solver.get_unsat_assumptions(&mut ctx).unwrap();
        assert!(core.contains(&act_lits[0]) && core.contains(&act_lits[2]));
    }

    /// Create an `UNSAT` query with an empty `UNSAT` assumptions
    #[test]
    fn test_unsat_assumptions_empty() {
        let backend = solver_from_env();
        if !backend.supports_get_unsat_assumptions() {
            return;
        }
        let mut ctx = Context::default();
        let a = ctx.bv_symbol("a", 3);
        let b = ctx.bv_symbol("b", 3);

        let eq3 = ctx.build(|c| c.equal(a, c.bit_vec_val(3, 3)));
        let eq4 = ctx.build(|c| c.equal(a, c.bit_vec_val(4, 3)));
        let b_is_1 = ctx.build(|c| c.equal(b, c.bit_vec_val(1, 3)));

        let mut solver = backend.start(None).unwrap();
        solver.set_logic(Logic::QfBv).unwrap();
        solver.declare_const(&ctx, a).unwrap();
        solver.declare_const(&ctx, b).unwrap();

        solver.assert(&ctx, eq3).unwrap();
        solver.assert(&ctx, eq4).unwrap();
        solver.assert(&ctx, b_is_1).unwrap();

        let res = solver.check_sat_assuming(&ctx, [b_is_1]).unwrap();
        assert_eq!(res, CheckSatResponse::Unsat);

        let core = solver.get_unsat_assumptions(&mut ctx).unwrap();
        assert!(core.is_empty());
    }

    /// Simulate pushing and popping context in the solver
    /// Check that variables in parent contexts persist in child contexts,
    /// while variables in popped contexts cannot be accessed anymore
    #[test]
    fn test_push_pop() {
        let backend = solver_from_env();
        if !backend.supports_get_unsat_assumptions() {
            return;
        }
        let mut ctx = Context::default();
        let x = ctx.bv_symbol("x", 3);
        let eq2 = ctx.build(|c| c.equal(x, c.bit_vec_val(2, 3)));
        let ge5 = ctx.build(|c| c.greater_or_equal(x, c.bit_vec_val(5, 3)));
        let ge1 = ctx.build(|c| c.greater_or_equal(x, c.bit_vec_val(1, 3)));

        let mut solver = backend.start(None).unwrap();
        solver.set_logic(Logic::QfBv).unwrap();

        solver.declare_const(&ctx, x).unwrap();
        let res = solver.check_sat_assuming(&ctx, [eq2, ge5, ge1]).unwrap();
        assert_eq!(res, CheckSatResponse::Unsat);

        // {eq2, ge5} is itself UNSAT, so a sufficient core must contain both.
        // Cores need not be minimal, so redundant assumptions may also appear.
        let core = solver.get_unsat_assumptions(&mut ctx).unwrap();
        assert!(core.contains(&eq2) && core.contains(&ge5));

        solver.push().unwrap();

        let y = ctx.bv_symbol("y", 3);
        let y_is_1 = ctx.build(|c| c.equal(y, c.bit_vec_val(1, 3)));

        solver.declare_const(&ctx, y).unwrap();
        let res = solver
            .check_sat_assuming(&ctx, [y_is_1, eq2, ge5, ge1])
            .unwrap();
        assert_eq!(res, CheckSatResponse::Unsat);

        // {eq2, ge5} is itself UNSAT, so a sufficient core must contain both.
        // Cores need not be minimal, so redundant assumptions may also appear.
        let core = solver.get_unsat_assumptions(&mut ctx).unwrap();
        assert!(core.contains(&eq2) && core.contains(&ge5));

        solver.push().unwrap();

        let y_is_2 = ctx.build(|c| c.equal(y, c.bit_vec_val(2, 3)));
        let res = solver.check_sat_assuming(&ctx, [y_is_1, y_is_2]).unwrap();
        assert_eq!(res, CheckSatResponse::Unsat);

        let core = solver.get_unsat_assumptions(&mut ctx).unwrap();
        assert_eq!(core.len(), 2);
        assert!(core.contains(&y_is_1) && core.contains(&y_is_2));

        solver.pop().unwrap();

        solver.push().unwrap();

        let z = ctx.bv_symbol("z", 3);
        let z_is_1 = ctx.build(|c| c.equal(z, c.bit_vec_val(1, 3)));
        let z_is_2 = ctx.build(|c| c.equal(z, c.bit_vec_val(2, 3)));

        solver.declare_const(&ctx, z).unwrap();

        let res = solver
            .check_sat_assuming(&ctx, [z_is_1, z_is_2, y_is_1])
            .unwrap();
        assert_eq!(res, CheckSatResponse::Unsat);

        // {z_is_1, z_is_2} is itself UNSAT, so a sufficient core must contain both.
        // Cores need not be minimal, so the unrelated `y_is_1` may also appear.
        let core = solver.get_unsat_assumptions(&mut ctx).unwrap();
        assert!(core.contains(&z_is_1) && core.contains(&z_is_2));

        solver.pop().unwrap();
        solver.pop().unwrap();

        let err = solver.check_sat_assuming(&ctx, [y_is_1, y_is_2]);
        assert!(err.is_err());
    }

    /// Check that assertions persist in child contexts
    #[test]
    fn test_assert_over_push_pop() {
        let mut ctx = Context::default();
        let x = ctx.bv_symbol("x", 3);
        let eq2 = ctx.build(|c| c.equal(x, c.bit_vec_val(2, 3)));

        let mut solver = solver_from_env().start(None).unwrap();
        solver.set_logic(Logic::QfBv).unwrap();
        solver.declare_const(&ctx, x).unwrap();
        solver.assert(&ctx, eq2).unwrap();

        solver.push().unwrap();

        let eq3 = ctx.build(|c| c.equal(x, c.bit_vec_val(3, 3)));
        solver.assert(&ctx, eq3).unwrap();
        let res = solver.check_sat().unwrap();
        assert_eq!(res, CheckSatResponse::Unsat);

        solver.pop().unwrap();
    }

    /// Check that `(get-unsat-assumptions)` fails after non-`UNSAT` query
    #[test]
    fn test_unsat_assumptions_fail() {
        let backend = solver_from_env();
        if !backend.supports_get_unsat_assumptions() {
            return;
        }
        let mut ctx = Context::default();
        let x = ctx.bv_symbol("x", 3);
        let eq2 = ctx.build(|c| c.equal(x, c.bit_vec_val(2, 3)));

        let mut solver = backend.start(None).unwrap();
        solver.set_logic(Logic::QfBv).unwrap();
        solver.declare_const(&ctx, x).unwrap();

        let res = solver.check_sat_assuming(&ctx, [eq2]).unwrap();
        assert_eq!(res, CheckSatResponse::Sat);

        let core = solver.get_unsat_assumptions(&mut ctx);
        assert!(core.is_err());

        let eq3 = ctx.build(|c| c.equal(x, c.bit_vec_val(3, 3)));
        let res = solver.check_sat_assuming(&ctx, [eq2, eq3]).unwrap();
        assert_eq!(res, CheckSatResponse::Unsat);

        let core = solver.get_unsat_assumptions(&mut ctx).unwrap();
        assert_eq!(core.len(), 2);
        assert!(core.contains(&eq2) && core.contains(&eq3));
    }

    #[test]
    fn test_restart() {
        let mut ctx = Context::default();
        let a = ctx.bv_symbol("a", 3);
        let mut solver = solver_from_env().start(None).unwrap();
        solver.set_logic(Logic::QfBv).unwrap();
        let three = ctx.bit_vec_val(3, 3);
        let four = ctx.bit_vec_val(3, 3);
        solver.define_const(&ctx, a, three).unwrap();
        let _res = solver.check_sat().unwrap();
        let value_of_a = solver.get_value(&mut ctx, a).unwrap();
        assert_eq!(value_of_a, three);

        // restarting the solver allows us to redefine `a`
        solver.restart().unwrap();
        // restart resets the logic too, so set it again for solvers that need it
        solver.set_logic(Logic::QfBv).unwrap();
        solver.define_const(&ctx, a, four).unwrap();
        let _res = solver.check_sat().unwrap();
        let value_of_a = solver.get_value(&mut ctx, a).unwrap();
        assert_eq!(value_of_a, four);
    }
}