From: ajreynol Date: Tue, 9 Feb 2016 22:57:50 +0000 (-0600) Subject: Fix regression, minor change to output. X-Git-Tag: cvc5-1.0.0~6081^2~4 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8194c44801d30c0e0aa6129490e0523851b24209;p=cvc5.git Fix regression, minor change to output. --- diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 8bc9689bd..560f68810 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -976,6 +976,16 @@ Node TermDb::mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& argTypes if( f.hasAttribute(InstLevelAttribute()) ){ theory::QuantifiersEngine::setInstantiationLevelAttr( ret, f.getAttribute(InstLevelAttribute()) ); } + + if( Trace.isOn("quantifiers-sk") ){ + Trace("quantifiers-sk") << "Skolemize : "; + for( unsigned i=0; igetTheoryEngine()->getSortInference()->setSkolemVar( f, f[0][i], d_skolem_constants[f][i] ); } } - if( Trace.isOn("quantifiers-sk") ){ - Trace("quantifiers-sk") << "Skolemize : "; - for( unsigned i=0; i