Add branch and bound lemma if linear arithmetic generates a non-integer assignment (#6868)smtcomp2021-fixed

This double checks that TheoryArithPrivate generates a model that does not assign real values to integer variables.

This is done outside of TheoryArithPrivate intentionally, so that it can be checked independently.

This code should very rarely be applied but would have caught the incorrect model which led to wrong results in the UFNIA division of smtcomp 2021.

1 files changed, 5 insertions, 4 deletions

diff --git a/src/theory/arith/arith_state.cpp b/src/theory/arith/arith_state.cpp
index 4af7b8b8d..93d410bf8 100644
--- a/src/theory/arith/arith_state.cpp
+++ b/src/theory/arith/arith_state.cpp
@@ -21,19 +21,20 @@ namespace cvc5 {
 namespace theory {
 namespace arith {
 
-ArithState::ArithState(TheoryArithPrivate& parent,
-                       context::Context* c,
+ArithState::ArithState(context::Context* c,
                        context::UserContext* u,
                        Valuation val)
-    : TheoryState(c, u, val), d_parent(parent)
+    : TheoryState(c, u, val), d_parent(nullptr)
 {
 }
 
 bool ArithState::isInConflict() const
 {
-  return d_parent.anyConflict() || d_conflict;
+  return d_parent->anyConflict() || d_conflict;
 }
 
+void ArithState::setParent(TheoryArithPrivate* p) { d_parent = p; }
+
 }  // namespace arith
 }  // namespace theory
 }  // namespace cvc5