Do not solve for 0-ary non-constant symbols (for which isVar returns true), add regressions.

2 files changed, 8 insertions, 2 deletions

diff --git a/src/expr/node.h b/src/expr/node.h
index 6dbb5aa2b..31721b2ef 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -464,6 +464,12 @@ public:
     assertTNodeNotExpired();
     return getMetaKind() == kind::metakind::VARIABLE;
   }
+  inline bool isUninterpretedVar() const {
+    assertTNodeNotExpired();
+    return getMetaKind() == kind::metakind::VARIABLE &&
+           getKind() != kind::UNIVERSE_SET && 
+           getKind() != kind::SEP_NIL;
+  }
 
   inline bool isClosure() const {
     assertTNodeNotExpired();
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 37d65972e..2b2ebbf5e 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -271,12 +271,12 @@ Theory::PPAssertStatus Theory::ppAssert(TNode in,
     // 1) x is a variable
     // 2) x is not in the term t
     // 3) x : T and t : S, then S <: T
-    if (in[0].isVar() && !in[1].hasSubterm(in[0]) &&
+    if (in[0].isUninterpretedVar() && !in[1].hasSubterm(in[0]) &&
         (in[1].getType()).isSubtypeOf(in[0].getType()) ){
       outSubstitutions.addSubstitution(in[0], in[1]);
       return PP_ASSERT_STATUS_SOLVED;
     }
-    if (in[1].isVar() && !in[0].hasSubterm(in[1]) &&
+    if (in[1].isUninterpretedVar() && !in[0].hasSubterm(in[1]) &&
         (in[0].getType()).isSubtypeOf(in[1].getType())){
       outSubstitutions.addSubstitution(in[1], in[0]);
       return PP_ASSERT_STATUS_SOLVED;