Fix bug in unconstrained simplifier related to sep.nil/distinguished variables.

diff --git a/src/theory/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp
index 6a33adc56dc67ba55930a60994349347312824e7..393a7c55901945fe63b627cf777020a6d23bc82b 100644 (file)
--- a/src/theory/unconstrained_simplifier.cpp
+++ b/src/theory/unconstrained_simplifier.cpp
@@ -79,7 +79,7 @@ void UnconstrainedSimplifier::visitAll(TNode assertion)
     d_visitedOnce[current] = parent;
 
     if (current.getNumChildren() == 0) {
-      if (current.isVar()) {
+      if (current.getKind()==kind::VARIABLE || current.getKind()==kind::SKOLEM) {
         d_unconstrained.insert(current);
       }
     }

diff --git a/test/regress/regress0/sep/trees-1.smt2 b/test/regress/regress0/sep/trees-1.smt2
index 88e875f704d542f5cbe03d0463993d8a7fbe4c81..8a46d9fddf7b3978793487d8e6db0c7b0e8b754b 100644 (file)
--- a/test/regress/regress0/sep/trees-1.smt2
+++ b/test/regress/regress0/sep/trees-1.smt2
@@ -1,4 +1,4 @@
-(set-logic ALL_SUPPORTED)
+(set-logic QF_ALL_SUPPORTED)
 (set-info :status unsat)
 
 (declare-sort Loc 0)