Skip to content

Incremental Interface adding Clauses to an empty solver causes undefined behavior #298

Description

@XeroOl

Create a project:

cargo new repro
cd repro
cargo add splr --features incremental_solver

Write code that adds clauses incrementally; not from a .cnf file:

use splr::{SatSolverIF, SolveIF, Solver};

fn main() {
    let mut s = Solver::default();
    for _ in 0..3 {
        s.add_var();
    }
    s.add_clause([1, 2]).unwrap();
    s.add_clause([1, 3]).unwrap();
    s.add_clause([2, 3]).unwrap();
    s.add_clause([-1, -2, -3]).unwrap();
    println!("{:?}", s.solve().unwrap());
}

run the code:

cargo run

I would expect something like Certificate::SAT([1, 2, -3]), but instead, I get a debug assertion:

thread 'main' panicked at library/core/src/panicking.rs:225:5:
unsafe precondition(s) violated: NonZero::new_unchecked requires the argument to be non-zero

This indicates a bug in the program. This Undefined Behavior check is optional, and cannot be relied on for safety.
stack backtrace:
   0: __rustc::rust_begin_unwind
             at /rustc/3e674b06b5c74adea662bd0b0b06450757994b16/library/std/src/panicking.rs:697:5
   1: core::panicking::panic_nounwind_fmt::runtime
             at /rustc/3e674b06b5c74adea662bd0b0b06450757994b16/library/core/src/panicking.rs:117:22
   2: core::panicking::panic_nounwind_fmt
             at /rustc/3e674b06b5c74adea662bd0b0b06450757994b16/library/core/src/intrinsics/mod.rs:3174:9
   3: core::panicking::panic_nounwind
             at /rustc/3e674b06b5c74adea662bd0b0b06450757994b16/library/core/src/panicking.rs:225:5
   4: core::num::nonzero::NonZero<T>::new_unchecked::precondition_check
             at /home/xerool/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ub_checks.rs:68:21
   5: core::num::nonzero::NonZero<T>::new_unchecked
             at /home/xerool/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ub_checks.rs:75:17
   6: splr::cdb::cid::<impl core::convert::From<usize> for splr::cdb::ClauseId>::from
             at /home/xerool/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/splr-0.17.2/src/cdb/cid.rs:26:31
   7: splr::cdb::db::<impl splr::cdb::ClauseDBIF for splr::cdb::ClauseDB>::new_clause
             at /home/xerool/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/splr-0.17.2/src/cdb/db.rs:292:19
   8: splr::solver::build::<impl splr::solver::Solver>::add_unchecked_clause
             at /home/xerool/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/splr-0.17.2/src/solver/build.rs:310:18
   9: <splr::solver::Solver as splr::solver::build::SatSolverIF>::add_clause
             at /home/xerool/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/splr-0.17.2/src/solver/build.rs:211:12
  10: repro::main
             at ./src/main.rs:8:5
  11: core::ops::function::FnOnce::call_once
             at /home/xerool/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ops/function.rs:250:5
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.
thread caused non-unwinding panic. aborting.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions