diff --git a/Cargo.lock b/Cargo.lock index 157337c8..7a011dab 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -111,7 +111,7 @@ dependencies = [ [[package]] name = "hoice" -version = "1.7.0" +version = "1.7.1" dependencies = [ "ansi_term 0.11.0 (registry+https://github.com/rust-lang/crates.io-index)", "atty 0.2.11 (registry+https://github.com/rust-lang/crates.io-index)", diff --git a/src/data/mod.rs b/src/data/mod.rs index f2436894..c649519b 100644 --- a/src/data/mod.rs +++ b/src/data/mod.rs @@ -805,9 +805,11 @@ impl Data { profile! { self mark "add cstr", "pre-checks" } profile! { self "trivial constraints" => add 1 } // Positive, constraint is trivial. + log! { @5 "rhs positive, trivial" } return Ok(None); } else if args.set_subsumed(&self.neg[pred]) { // Negative, ignore. + log! { @5 "rhs negative, discarding rhs" } None } else { Some(args) @@ -832,7 +834,7 @@ impl Data { if args.set_subsumed(&self.pos[pred]) { self.register_raw_sample_dep(pred, &args, &nu_rhs)?; // Is this the last (positive) sample in a `... => false` constraint? - if nu_rhs.is_none() && lhs.is_empty() { + if nu_rhs.is_none() && lhs.is_empty() && nu_lhs.is_empty() { // Then register as negative to record the conflict. self.add_neg(clause, pred, args); unsat!("by `true => false` in constraint (data, prune_cstr)")