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, 4 insertions, 5 deletions

diff --git a/src/theory/arith/arith_state.h b/src/theory/arith/arith_state.h
index 0aa848f46..a54ae6bf0 100644
--- a/src/theory/arith/arith_state.h
+++ b/src/theory/arith/arith_state.h
@@ -38,17 +38,16 @@ class TheoryArithPrivate;
 class ArithState : public TheoryState
 {
  public:
-  ArithState(TheoryArithPrivate& parent,
-             context::Context* c,
-             context::UserContext* u,
-             Valuation val);
+  ArithState(context::Context* c, context::UserContext* u, Valuation val);
   ~ArithState() {}
   /** Are we currently in conflict? */
   bool isInConflict() const override;
+  /** Set parent */
+  void setParent(TheoryArithPrivate* p);
 
  private:
   /** reference to parent */
-  TheoryArithPrivate& d_parent;
+  TheoryArithPrivate* d_parent;
 };
 
 }  // namespace arith