Bug fix, doc

1 files changed, 12 insertions, 1 deletions

diff --git a/src/smt/model_blocker.h b/src/smt/model_blocker.h
index cc667fbf0..ce80d2144 100644
--- a/src/smt/model_blocker.h
+++ b/src/smt/model_blocker.h
@@ -36,7 +36,18 @@ class ModelBlocker
    * This returns a disjunction of literals ~L1 V ... V ~Ln with the following
    * properties:
    * (1) L1 ... Ln hold in the current model (given by argument m),
-   * (2) L1 ... Ln are literals that occur in assertions.
+   * (2) L1 ... Ln are literals that occur in assertions and propositionally
+   * entail all non-unit top-level assertions.
+   * 
+   * For example, if our input is:
+   *    x > 0 ^ ( y < 0 V z < 0 V w < 0 )
+   * and m is { x -> 1, y -> 2, z -> -1, w -> -1 }, then this method may
+   * return ~(z < 0) or ~(w < 0).
+   * 
+   * Notice that we do not require that L1...Ln entail unit top-level assertions
+   * since these literals are trivially entailed to be true in all models of
+   * our input. In other words, we do not return ~(x < 0) V ~(w < 0) since the
+   * left disjunct is always false.
    */
   static Expr getModelBlocker(const std::vector<Expr>& assertions, Model* m);
 }; /* class TheoryModelCoreBuilder */