From 14fb8fac59e368a36e936a2d0497745eda72c637 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 9 Sep 2016 15:01:20 -0500 Subject: [PATCH] Fix bug in unconstrained simplifier related to sep.nil/distinguished variables. --- src/theory/unconstrained_simplifier.cpp | 2 +- test/regress/regress0/sep/trees-1.smt2 | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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) -- 2.30.2