Added preprocessing pass that propagates unconstrained values - solves all of

the unconstrained examples in QF_AUFBV/brummayerbiere3 - should also help
generally on at least BV and maybe others.
Off by default for now - results are mixed and it's hard to evaluate with so
many existing assertion failures and segfaults - will re-evaluate once those
are fixed

1 files changed, 9 insertions, 0 deletions

diff --git a/src/expr/node.h b/src/expr/node.h
index 4d39ec60f..3532116bc 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -451,6 +451,15 @@ public:
   }
 
   /**
+   * Returns true if this node represents a constant
+   * @return true if const
+   */
+  inline bool isVar() const {
+    assertTNodeNotExpired();
+    return getMetaKind() == kind::metakind::VARIABLE;
+  }
+
+  /**
    * Returns the unique id of this node
    * @return the ud
    */