diff options
| author | Liana Hadarean <lianahady@gmail.com> | 2012-04-04 02:02:06 +0000 |
|---|---|---|
| committer | Liana Hadarean <lianahady@gmail.com> | 2012-04-04 02:02:06 +0000 |
| commit | 52d6dc20c61007a5c066590aa1fd0b95ed3c2527 (patch) | |
| tree | 040efec36cde7775b5c19eb43fcdd60cbeb61f9e /src/prop/minisat | |
| parent | 4fa8c7d1a0654e7780fd485c51463c06b34379b5 (diff) | |
* added propagation as lemmas to TheoryBV:
* modified BVMinisat to work incrementally
* added more bv regressions
Diffstat (limited to 'src/prop/minisat')
| -rw-r--r-- | src/prop/minisat/core/Solver.cc | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 3a16b0d19..c602d8b9c 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -195,6 +195,8 @@ CRef Solver::reason(Var x) { if (varLevel > explLevel) { explLevel = varLevel; } + Assert(value(explanation[i]) != l_Undef); + Assert(i == 0 || trail_index(var(explanation[0])) > trail_index(var(explanation[i]))); } // Construct the reason (level 0) |