From 2c208e1d1002c25593ad2e1a637fdfe96628fda3 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 30 Apr 2017 10:23:00 -0700
Subject: [PATCH] Sat update
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/sat/sat_solver.cpp | 3 +++
1 file changed, 3 insertions(+)
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 739a591e7..cd13ac7a4 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -3291,6 +3291,9 @@ namespace sat {
literal lit = *it;
if (value(lit) != l_undef) {
++num_fixed;
+ if (value(lit) == l_true && lvl(lit) == 1) {
+ VERIFY(extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq));
+ }
continue;
}
push();