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

6 files changed, 46 insertions, 4 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;
diff --git a/test/regress/regress0/rels/Makefile.am b/test/regress/regress0/rels/Makefile.am
index 06658e988..7c9dca8dd 100644
--- a/test/regress/regress0/rels/Makefile.am
+++ b/test/regress/regress0/rels/Makefile.am
@@ -100,7 +100,8 @@ TESTS =	\
   rel_tp_join_1.cvc \
   rel_transpose_0.cvc \
   set-strat.cvc \
-  rel_tc_8.cvc
+  rel_tc_8.cvc \
+  atom_univ2.cvc
 
 # unsolved : garbage_collect.cvc
 
diff --git a/test/regress/regress0/rels/atom_univ2.cvc b/test/regress/regress0/rels/atom_univ2.cvc
new file mode 100644
index 000000000..9901ce630
--- /dev/null
+++ b/test/regress/regress0/rels/atom_univ2.cvc
@@ -0,0 +1,23 @@
+% EXPECT: unsat

+OPTION "logic" "ALL_SUPPORTED";

+Atom: TYPE;

+

+a : SET OF [Atom];

+b : SET OF [Atom, Atom];

+

+x : Atom;

+y : Atom;

+

+ASSERT NOT(x = y);

+

+ASSERT TUPLE(y) IS_IN a;

+ASSERT (x, y) IS_IN b;

+

+ASSERT UNIVERSE::SET OF [Atom, Atom] = (UNIVERSE::SET OF [Atom] PRODUCT UNIVERSE::SET OF [Atom]);

+

+u : SET OF [Atom, Atom];

+ASSERT u = UNIVERSE::SET OF [Atom, Atom];

+

+ASSERT NOT (x, y) IS_IN u;

+

+CHECKSAT;

diff --git a/test/regress/regress0/sep/Makefile.am b/test/regress/regress0/sep/Makefile.am
index f731bd15e..692390dde 100644
--- a/test/regress/regress0/sep/Makefile.am
+++ b/test/regress/regress0/sep/Makefile.am
@@ -56,7 +56,8 @@ TESTS =	\
   emp2-quant-unsat.smt2 \
   dispose-1.smt2 \
   finite-witness-sat.smt2 \
-  sep-fmf-priority.smt2
+  sep-fmf-priority.smt2 \
+  nil-no-elim.smt2
 
 
 FAILING_TESTS =
diff --git a/test/regress/regress0/sep/nil-no-elim.smt2 b/test/regress/regress0/sep/nil-no-elim.smt2
new file mode 100644
index 000000000..e9aa3807a
--- /dev/null
+++ b/test/regress/regress0/sep/nil-no-elim.smt2
@@ -0,0 +1,11 @@
+(set-logic ALL)
+(set-info :status unsat)
+(declare-sort U 0)
+(declare-fun f (U) U)
+(declare-fun a () U)
+
+(assert (= (as sep.nil U) (f a)))
+
+(assert (pto (f a) 0))
+
+(check-sat)