From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 9 Sep 2016 20:01:20 +0000 (-0500)
Subject: Fix bug in unconstrained simplifier related to sep.nil/distinguished variables.
X-Git-Tag: cvc5-1.0.0~6028^2~58
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=14fb8fac59e368a36e936a2d0497745eda72c637;p=cvc5.git

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 6a33adc56..393a7c559 100644
--- 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 88e875f70..8a46d9fdd 100644
--- 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)