From d288f52dd82fe6590950758289e86ebcb039350d Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Wed, 30 Jun 2021 15:07:47 -0700
Subject: [PATCH] Use SAT context level for --bv-assert-input instead of
 decision level. (#6758)

The decision level as previously implemented was not accurate since it
did not consider the user context level. This resulted in facts being
incorrectly recognized as input assertions, which happened for
incremental benchmarks.
---
 src/prop/minisat/minisat.cpp         |  2 +-
 src/prop/minisat/minisat.h           | 11 ++++++++++-
 src/prop/prop_engine.h               |  2 +-
 src/theory/bv/bv_solver_bitblast.cpp |  4 ++--
 src/theory/valuation.h               |  2 +-
 test/regress/CMakeLists.txt          |  1 +
 test/regress/regress0/issue6738.smt2 | 12 ++++++++++++
 7 files changed, 28 insertions(+), 6 deletions(-)
 create mode 100644 test/regress/regress0/issue6738.smt2

diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 4adbbe7f7..e193bfb28 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -260,7 +260,7 @@ bool MinisatSatSolver::isDecision(SatVariable decn) const {
 
 int32_t MinisatSatSolver::getDecisionLevel(SatVariable v) const
 {
-  return d_minisat->level(v);
+  return d_minisat->level(v) + d_minisat->user_level(v);
 }
 
 int32_t MinisatSatSolver::getIntroLevel(SatVariable v) const
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index 15ef5cacb..984cc6479 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -93,11 +93,20 @@ class MinisatSatSolver : public CDCLTSatSolverInterface
 
   bool isDecision(SatVariable decn) const override;
 
+  /** Return decision level at which `lit` was decided on. */
   int32_t getDecisionLevel(SatVariable v) const override;
 
+  /**
+   * Return user level at which `lit` was introduced.
+   *
+   * Note: The user level is tracked independently in the SAT solver and does
+   * not query the user-context for the user level. The user level in the SAT
+   * solver starts at level 0 and does not include the global push/pop in
+   * the SMT engine.
+   */
   int32_t getIntroLevel(SatVariable v) const override;
 
-  /** Retrieve a pointer to the unerlying solver. */
+  /** Retrieve a pointer to the underlying solver. */
   Minisat::SimpSolver* getSolver() { return d_minisat; }
 
   /** Retrieve the proof manager of this SAT solver. */
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 74da49cf6..e458ca5e5 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -157,7 +157,7 @@ class PropEngine
   bool isDecision(Node lit) const;
 
   /**
-   * Return the current decision level of `lit`.
+   * Return SAT context level at which `lit` was decided on.
    *
    * @param lit: The node in question, must have an associated SAT literal.
    * @return Decision level of the SAT variable of `lit` (phase is disregarded),
diff --git a/src/theory/bv/bv_solver_bitblast.cpp b/src/theory/bv/bv_solver_bitblast.cpp
index 3ae4a7f0a..a5d89e371 100644
--- a/src/theory/bv/bv_solver_bitblast.cpp
+++ b/src/theory/bv/bv_solver_bitblast.cpp
@@ -219,9 +219,9 @@ bool BVSolverBitblast::preNotifyFact(
    * using assumptions.
    */
   if (options::bvAssertInput() && val.isSatLiteral(fact)
-      && !val.isDecision(fact) && val.getDecisionLevel(fact) == 0
-      && val.getIntroLevel(fact) == 0)
+      && val.getDecisionLevel(fact) == 0 && val.getIntroLevel(fact) == 0)
   {
+    Assert(!val.isDecision(fact));
     d_bbInputFacts.push_back(fact);
   }
   else
diff --git a/src/theory/valuation.h b/src/theory/valuation.h
index 7438279b1..192b5dfc8 100644
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -185,7 +185,7 @@ public:
   bool isDecision(Node lit) const;
 
   /**
-   * Return the current decision level of `lit`.
+   * Return SAT context level at which `lit` was decided on.
    *
    * @param lit: The node in question, must have an associated SAT literal.
    * @return Decision level of the SAT variable of `lit` (phase is disregarded),
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index fe49d8b39..e2e216567 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -674,6 +674,7 @@ set(regress_0_tests
   regress0/issue5743.smt2
   regress0/issue5947.smt2
   regress0/issue6605-2-abd-triv.smt2
+  regress0/issue6738.smt2
   regress0/issue6741.smt2
   regress0/ite_arith.smt2
   regress0/ite_real_int_type.smtv1.smt2
diff --git a/test/regress/regress0/issue6738.smt2 b/test/regress/regress0/issue6738.smt2
new file mode 100644
index 000000000..905ae823c
--- /dev/null
+++ b/test/regress/regress0/issue6738.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: -i --bv-solver=bitblast --bv-assert-input
+(set-logic QF_BV)
+(declare-fun N () Bool)
+(assert (not (= (_ bv1 1) (bvnot (ite N (_ bv1 1) (_ bv0 1))))))
+(push 1)
+(assert (not N))
+(set-info :status unsat)
+(check-sat)
+(pop 1)
+(set-info :status sat)
+(check-sat)
+
-- 
2.30.2