/** Is this node constant? (and has that been computed yet?) */
struct IsConstTag { };
struct IsConstComputedTag { };
+struct HasBoundVarTag { };
+struct HasBoundVarComputedTag { };
typedef expr::Attribute<IsConstTag, bool> IsConstAttr;
typedef expr::Attribute<IsConstComputedTag, bool> IsConstComputedAttr;
+/** Attribute true for expressions with bound variables in them */
+typedef expr::Attribute<HasBoundVarTag, bool> HasBoundVarAttr;
+typedef expr::Attribute<HasBoundVarComputedTag, bool> HasBoundVarComputedAttr;
template <bool ref_count>
bool NodeTemplate<ref_count>::isConst() const {
}
}
+template <bool ref_count>
+bool NodeTemplate<ref_count>::hasBoundVar() {
+ assertTNodeNotExpired();
+ if(! getAttribute(HasBoundVarComputedAttr())) {
+ bool hasBv = false;
+ if(getKind() == kind::BOUND_VARIABLE) {
+ hasBv = true;
+ } else {
+ for(iterator i = begin(); i != end() && !hasBv; ++i) {
+ hasBv = (*i).hasBoundVar();
+ }
+ }
+ setAttribute(HasBoundVarAttr(), hasBv);
+ setAttribute(HasBoundVarComputedAttr(), true);
+ Debug("bva") << *this << " has bva : " << getAttribute(HasBoundVarAttr()) << std::endl;
+ return hasBv;
+ }
+ return getAttribute(HasBoundVarAttr());
+}
+
template bool NodeTemplate<true>::isConst() const;
template bool NodeTemplate<false>::isConst() const;
+template bool NodeTemplate<true>::hasBoundVar();
+template bool NodeTemplate<false>::hasBoundVar();
}/* CVC4 namespace */
// bool containsDecision(); // is "atomic"
// bool properlyContainsDecision(); // maybe not atomic but all children are
+ /**
+ * Returns true iff this node contains a bound variable. This bound
+ * variable may or may not be free.
+ * @return true iff this node contains a bound variable.
+ */
+ bool hasBoundVar();
+
/**
* Convert this Node into an Expr using the currently-in-scope
* manager. Essentially this is like an "operator Expr()" but we
continue;
}
+ // Replace the already-known ITEs (this is important for ground ITEs under quantifiers).
+ n = d_private->d_iteRemover.replace(n);
+ Notice() << "SmtEngine::checkModel(): -- ite replacement gives " << n << endl;
+
// As a last-ditch effort, ask model to simplify it.
// Presently, this is only an issue for quantifiers, which can have a value
// but don't show up in our substitution map above.
namespace theory {
namespace ite {
+
inline static bool isTermITE(TNode e) {
return (e.getKind() == kind::ITE && !e.getType().isBoolean());
}
} /* CVC4::theory::ite */
-
-
-ITEUtilities::ITEUtilities(ContainsTermITEVistor* containsVisitor)
+ITEUtilities::ITEUtilities(ContainsTermITEVisitor* containsVisitor)
: d_containsVisitor(containsVisitor)
, d_compressor(NULL)
, d_simplifier(NULL)
}
/********************* */
-/* ContainsTermITEVistor
+/* ContainsTermITEVisitor
*/
-ContainsTermITEVistor::ContainsTermITEVistor(): d_cache() {}
-ContainsTermITEVistor::~ContainsTermITEVistor(){}
-bool ContainsTermITEVistor::containsTermITE(TNode e){
+ContainsTermITEVisitor::ContainsTermITEVisitor(): d_cache() {}
+ContainsTermITEVisitor::~ContainsTermITEVisitor(){}
+bool ContainsTermITEVisitor::containsTermITE(TNode e){
/* throughout execution skip through NOT nodes. */
e = (e.getKind() == kind::NOT) ? e[0] : e;
if(ite::triviallyContainsNoTermITEs(e)){ return false; }
}
return foundTermIte;
}
-void ContainsTermITEVistor::garbageCollect() {
+void ContainsTermITEVisitor::garbageCollect() {
d_cache.clear();
}
/********************* */
/* ITECompressor
*/
-ITECompressor::ITECompressor(ContainsTermITEVistor* contains)
+ITECompressor::ITECompressor(ContainsTermITEVisitor* contains)
: d_contains(contains)
, d_assertions(NULL)
, d_incoming(true, true)
-ITESimplifier::ITESimplifier(ContainsTermITEVistor* contains)
+ITESimplifier::ITESimplifier(ContainsTermITEVisitor* contains)
: d_containsVisitor(contains)
, d_termITEHeight()
, d_constantLeaves()
return substitute(e, substTable, cache);
}
-
} /* namespace theory */
} /* namespace CVC4 */
namespace CVC4 {
namespace theory {
-class ContainsTermITEVistor;
+class ContainsTermITEVisitor;
class IncomingArcCounter;
class TermITEHeightCounter;
class ITECompressor;
class ITEUtilities {
public:
- ITEUtilities(ContainsTermITEVistor* containsVisitor);
+ ITEUtilities(ContainsTermITEVisitor* containsVisitor);
~ITEUtilities();
Node simpITE(TNode assertion);
void clear();
private:
- ContainsTermITEVistor* d_containsVisitor;
+ ContainsTermITEVisitor* d_containsVisitor;
ITECompressor* d_compressor;
ITESimplifier* d_simplifier;
ITECareSimplifier* d_careSimp;
/**
* A caching visitor that computes whether a node contains a term ite.
*/
-class ContainsTermITEVistor {
+class ContainsTermITEVisitor {
public:
- ContainsTermITEVistor();
- ~ContainsTermITEVistor();
+ ContainsTermITEVisitor();
+ ~ContainsTermITEVisitor();
/** returns true if a node contains a term ite. */
bool containsTermITE(TNode n);
*/
class ITECompressor {
public:
- ITECompressor(ContainsTermITEVistor* contains);
+ ITECompressor(ContainsTermITEVisitor* contains);
~ITECompressor();
/* returns false if an assertion is discovered to be equal to false. */
Node d_true; /* Copy of true. */
Node d_false; /* Copy of false. */
- ContainsTermITEVistor* d_contains;
+ ContainsTermITEVisitor* d_contains;
std::vector<Node>* d_assertions;
IncomingArcCounter d_incoming;
class ITESimplifier {
public:
- ITESimplifier(ContainsTermITEVistor* d_containsVisitor);
+ ITESimplifier(ContainsTermITEVisitor* d_containsVisitor);
~ITESimplifier();
Node simpITE(TNode assertion);
Node d_true;
Node d_false;
- ContainsTermITEVistor* d_containsVisitor;
+ ContainsTermITEVisitor* d_containsVisitor;
inline bool containsTermITE(TNode n) {
return d_containsVisitor->containsTermITE(n);
}
for( unsigned i=0; i<d_set[f].size(); i++) {
Node v = d_set[f][i];
Node r = d_range[f][v];
- if( quantifiers::TermDb::hasBoundVarAttr(r) ){
+ if( r.hasBoundVar() ){
//introduce a new bound
Node new_range = NodeManager::currentNM()->mkSkolem( "bir_$$", r.getType(), "bound for term" );
d_nground_range[f][v] = d_range[f][v];
}
bool BoundedIntegers::isGroundRange(Node f, Node v) {
- return isBoundVar(f,v) && !quantifiers::TermDb::hasBoundVarAttr(getLowerBound(f,v)) && !quantifiers::TermDb::hasBoundVarAttr(getUpperBound(f,v));
+ return isBoundVar(f,v) && !getLowerBound(f,v).hasBoundVar() && !getUpperBound(f,v).hasBoundVar();
}
# forall x. P( x ) => f( S( x ) ) = x
option preSkolemQuant --pre-skolem-quant bool :read-write :default false
apply skolemization eagerly to bodies of quantified formulas
-option iteRemoveQuant --ite-remove-quant bool :default false
- apply ite removal to bodies of quantifiers
# Whether to perform agressive miniscoping
option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false
perform aggressive miniscoping for quantifiers
registerNode( n[1], hasPol, pol, true );\r
}else{\r
if( n.getKind()!=OR && n.getKind()!=AND && n.getKind()!=IFF && n.getKind()!=NOT ){\r
- if( quantifiers::TermDb::hasBoundVarAttr( n ) ){\r
+ if( n.hasBoundVar() ){\r
//literals\r
if( n.getKind()==EQUAL ){\r
for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
\r
void QuantInfo::flatten( Node n, bool beneathQuant ) {\r
Trace("qcf-qregister-debug2") << "Flatten : " << n << std::endl;\r
- if( quantifiers::TermDb::hasBoundVarAttr( n ) ){\r
+ if( n.hasBoundVar() ){\r
if( d_var_num.find( n )==d_var_num.end() ){\r
Trace("qcf-qregister-debug2") << "Add FLATTEN VAR : " << n << std::endl;\r
d_var_num[n] = d_vars.size();\r
d_type = typ_invalid;\r
}\r
}else{\r
- if( quantifiers::TermDb::hasBoundVarAttr( n ) ){\r
+ if( n.hasBoundVar() ){\r
d_type_not = false;\r
d_n = n;\r
if( d_n.getKind()==NOT ){\r
//literals\r
if( d_n.getKind()==EQUAL ){\r
for( unsigned i=0; i<2; i++ ){\r
- if( quantifiers::TermDb::hasBoundVarAttr( d_n[i] ) ){\r
+ if( d_n[i].hasBoundVar() ){\r
if( !qi->isVar( d_n[i] ) ){\r
Trace("qcf-qregister-debug") << "ERROR : not var " << d_n[i] << std::endl;\r
}else if( d_n[i].getKind()==BOUND_VARIABLE && !beneathQuant ){\r
}\r
}else if( d_type==typ_eq ){\r
for( unsigned i=0; i<d_n.getNumChildren(); i++ ){\r
- if( !quantifiers::TermDb::hasBoundVarAttr( d_n[i] ) ){\r
+ if( !d_n[i].hasBoundVar() ){\r
d_ground_eval[i] = p->evaluateTerm( d_n[i] );\r
}\r
}\r
eq::EqClassIterator eqc_i = eq::EqClassIterator( r, getEqualityEngine() );\r
while( !eqc_i.isFinished() ){\r
TNode n = (*eqc_i);\r
- if( quantifiers::TermDb::hasBoundVarAttr( n ) ){\r
+ if( n.hasBoundVar() ){\r
std::cout << "BAD TERM IN DB : " << n << std::endl;\r
exit( 199 );\r
}\r
// std::cout << n.getKind() << " " << n.getOperator() << " " << n << std::endl;\r
// }\r
//}\r
- if( !quantifiers::TermDb::hasBoundVarAttr( n ) ){ //temporary\r
+ if( !n.hasBoundVar() ){ //temporary\r
\r
bool isRedundant;\r
std::map< TNode, std::vector< TNode > >::iterator it_na;\r
StatisticsRegistry::unregisterStat(&d_partial_inst);\r
}\r
\r
-}
\ No newline at end of file
+}\r
return !getInstConstAttr(n).isNull();
}
-bool TermDb::hasBoundVarAttr( Node n ) {
- if( !n.getAttribute(HasBoundVarComputedAttribute()) ){
- bool hasBv = false;
- if( n.getKind()==BOUND_VARIABLE ){
- hasBv = true;
- }else{
- for (unsigned i=0; i<n.getNumChildren(); i++) {
- if( hasBoundVarAttr(n[i]) ){
- hasBv = true;
- break;
- }
- }
- }
- HasBoundVarAttribute hbva;
- n.setAttribute(hbva, hasBv);
- HasBoundVarComputedAttribute hbvca;
- n.setAttribute(hbvca, true);
- Trace("bva") << n << " has bva : " << n.getAttribute(HasBoundVarAttribute()) << std::endl;
- }
- return n.getAttribute(HasBoundVarAttribute());
-}
-
void TermDb::getBoundVars( Node n, std::vector< Node >& bvs) {
if (n.getKind()==BOUND_VARIABLE ){
if ( std::find( bvs.begin(), bvs.end(), n)==bvs.end() ){
struct ModelBasisArgAttributeId {};
typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t> ModelBasisArgAttribute;
-struct HasBoundVarAttributeId {};
-typedef expr::Attribute<HasBoundVarAttributeId, bool> HasBoundVarAttribute;
-struct HasBoundVarComputedAttributeId {};
-typedef expr::Attribute<HasBoundVarComputedAttributeId, bool> HasBoundVarComputedAttribute;
-
//for rewrite rules
struct QRewriteRuleAttributeId {};
typedef expr::Attribute<QRewriteRuleAttributeId, Node> QRewriteRuleAttribute;
static bool hasInstConstAttr( Node n );
//for bound variables
public:
- //does n have bound variables?
- static bool hasBoundVarAttr( Node n );
//get bound variables in n
static void getBoundVars( Node n, std::vector< Node >& bvs);
//for skolem
#include "util/ite_removal.h"
#include "expr/command.h"
-#include "theory/quantifiers/options.h"
#include "theory/ite_utilities.h"
using namespace CVC4;
RemoveITE::RemoveITE(context::UserContext* u)
: d_iteCache(u)
{
- d_containsVisitor = new theory::ContainsTermITEVistor();
+ d_containsVisitor = new theory::ContainsTermITEVisitor();
}
RemoveITE::~RemoveITE(){
d_containsVisitor->garbageCollect();
}
-theory::ContainsTermITEVistor* RemoveITE::getContainsVisitor(){
+theory::ContainsTermITEVisitor* RemoveITE::getContainsVisitor() {
return d_containsVisitor;
}
void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap)
{
for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) {
- std::vector<Node> quantVar;
// Do this in two steps to avoid Node problems(?)
// Appears related to bug 512, splitting this into two lines
// fixes the bug on clang on Mac OS
- Node itesRemoved = run(output[i], output, iteSkolemMap, quantVar);
+ Node itesRemoved = run(output[i], output, iteSkolemMap, false);
output[i] = itesRemoved;
}
}
-bool RemoveITE::containsTermITE(TNode e){
+bool RemoveITE::containsTermITE(TNode e) const {
return d_containsVisitor->containsTermITE(e);
}
Node RemoveITE::run(TNode node, std::vector<Node>& output,
- IteSkolemMap& iteSkolemMap,
- std::vector<Node>& quantVar) {
+ IteSkolemMap& iteSkolemMap, bool inQuant) {
// Current node
Debug("ite") << "removeITEs(" << node << ")" << endl;
}
// The result may be cached already
+ std::pair<Node, bool> cacheKey(node, inQuant);
NodeManager *nodeManager = NodeManager::currentNM();
- ITECache::const_iterator i = d_iteCache.find(node);
+ ITECache::const_iterator i = d_iteCache.find(cacheKey);
if(i != d_iteCache.end()) {
Node cached = (*i).second;
Debug("ite") << "removeITEs: in-cache: " << cached << endl;
return cached.isNull() ? Node(node) : cached;
}
+ // Remember that we're inside a quantifier
+ if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) {
+ inQuant = true;
+ }
+
// If an ITE replace it
if(node.getKind() == kind::ITE) {
TypeNode nodeType = node.getType();
- if(!nodeType.isBoolean()) {
+ if(!nodeType.isBoolean() && (!inQuant || !node.hasBoundVar())) {
+Debug("ite") << "CAN REMOVE ITE " << node << " BECAUSE " << inQuant << " " << node.hasBoundVar() << endl;
Node skolem;
// Make the skolem to represent the ITE
- if( quantVar.empty() ){
- skolem = nodeManager->mkSkolem("termITE_$$", nodeType, "a variable introduced due to term-level ITE removal");
- }else{
- //if in the scope of free variables, make a skolem operator
- vector< TypeNode > argTypes;
- for( size_t i=0; i<quantVar.size(); i++ ){
- argTypes.push_back( quantVar[i].getType() );
- }
- TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, nodeType );
- Node op = NodeManager::currentNM()->mkSkolem( "termITEop_$$", typ, "a function variable introduced due to term-level ITE removal" );
- vector< Node > funcArgs;
- funcArgs.push_back( op );
- funcArgs.insert( funcArgs.end(), quantVar.begin(), quantVar.end() );
- skolem = NodeManager::currentNM()->mkNode( kind::APPLY_UF, funcArgs );
- }
+ skolem = nodeManager->mkSkolem("termITE_$$", nodeType, "a variable introduced due to term-level ITE removal");
// The new assertion
Node newAssertion =
Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl;
// Attach the skolem
- d_iteCache.insert(node, skolem);
+ d_iteCache.insert(cacheKey, skolem);
// Remove ITEs from the new assertion, rewrite it and push it to the output
- newAssertion = run(newAssertion, output, iteSkolemMap, quantVar);
-
- if( !quantVar.empty() ){
- //if in the scope of free variables, it is a quantified assertion
- vector< Node > children;
- children.push_back( NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, quantVar ) );
- children.push_back( newAssertion );
- newAssertion = NodeManager::currentNM()->mkNode( kind::FORALL, children );
- }
+ newAssertion = run(newAssertion, output, iteSkolemMap, inQuant);
iteSkolemMap[skolem] = output.size();
output.push_back(newAssertion);
}
// If not an ITE, go deep
- if( ( node.getKind() != kind::FORALL || options::iteRemoveQuant() ) &&
- node.getKind() != kind::EXISTS &&
- node.getKind() != kind::REWRITE_RULE ) {
- std::vector< Node > newQuantVar;
- newQuantVar.insert( newQuantVar.end(), quantVar.begin(), quantVar.end() );
- if( node.getKind()==kind::FORALL ){
- for( size_t i=0; i<node[0].getNumChildren(); i++ ){
- newQuantVar.push_back( node[0][i] );
- }
- }
- vector<Node> newChildren;
- bool somethingChanged = false;
- if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
- newChildren.push_back(node.getOperator());
- }
- // Remove the ITEs from the children
- for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
- Node newChild = run(*it, output, iteSkolemMap, newQuantVar);
- somethingChanged |= (newChild != *it);
- newChildren.push_back(newChild);
- }
+ vector<Node> newChildren;
+ bool somethingChanged = false;
+ if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ newChildren.push_back(node.getOperator());
+ }
+ // Remove the ITEs from the children
+ for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
+ Node newChild = run(*it, output, iteSkolemMap, inQuant);
+ somethingChanged |= (newChild != *it);
+ newChildren.push_back(newChild);
+ }
- // If changes, we rewrite
- if(somethingChanged) {
- Node cached = nodeManager->mkNode(node.getKind(), newChildren);
- d_iteCache.insert(node, cached);
- return cached;
- } else {
- d_iteCache.insert(node, Node::null());
- return node;
- }
+ // If changes, we rewrite
+ if(somethingChanged) {
+ Node cached = nodeManager->mkNode(node.getKind(), newChildren);
+ d_iteCache.insert(cacheKey, cached);
+ return cached;
} else {
- d_iteCache.insert(node, Node::null());
+ d_iteCache.insert(cacheKey, Node::null());
return node;
}
}
+Node RemoveITE::replace(TNode node, bool inQuant) const {
+ if(node.isVar() || node.isConst() ||
+ (options::biasedITERemoval() && !containsTermITE(node))){
+ return Node(node);
+ }
+
+ // Check the cache
+ NodeManager *nodeManager = NodeManager::currentNM();
+ ITECache::const_iterator i = d_iteCache.find(make_pair(node, inQuant));
+ if(i != d_iteCache.end()) {
+ Node cached = (*i).second;
+ return cached.isNull() ? Node(node) : cached;
+ }
+
+ // Remember that we're inside a quantifier
+ if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) {
+ inQuant = true;
+ }
+
+ vector<Node> newChildren;
+ bool somethingChanged = false;
+ if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ newChildren.push_back(node.getOperator());
+ }
+ // Replace in children
+ for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) {
+ Node newChild = replace(*it, inQuant);
+ somethingChanged |= (newChild != *it);
+ newChildren.push_back(newChild);
+ }
+
+ // If changes, we rewrite
+ if(somethingChanged) {
+ return nodeManager->mkNode(node.getKind(), newChildren);
+ } else {
+ return node;
+ }
+}
}/* CVC4 namespace */
#include "util/dump.h"
#include "context/context.h"
#include "context/cdinsert_hashmap.h"
+#include "util/hash.h"
+#include "util/bool.h"
namespace CVC4 {
namespace theory {
-class ContainsTermITEVistor;
-}
+ class ContainsTermITEVisitor;
+}/* CVC4::theory namespace */
typedef std::hash_map<Node, unsigned, NodeHashFunction> IteSkolemMap;
class RemoveITE {
- typedef context::CDInsertHashMap<Node, Node, NodeHashFunction> ITECache;
+ typedef context::CDInsertHashMap< std::pair<Node, bool>, Node, PairHashFunction<Node, bool, NodeHashFunction, BoolHashFunction> > ITECache;
ITECache d_iteCache;
* ite created in conjunction with that skolem variable.
*/
Node run(TNode node, std::vector<Node>& additionalAssertions,
- IteSkolemMap& iteSkolemMap, std::vector<Node>& quantVar);
+ IteSkolemMap& iteSkolemMap, bool inQuant);
- /** Returns true if e contains a term ite.*/
- bool containsTermITE(TNode e);
+ /**
+ * Substitute under node using pre-existing cache. Do not remove
+ * any ITEs not seen during previous runs.
+ */
+ Node replace(TNode node, bool inQuant = false) const;
+
+ /** Returns true if e contains a term ite. */
+ bool containsTermITE(TNode e) const;
- /** Returns the collected size of the caches.*/
+ /** Returns the collected size of the caches. */
size_t collectedCacheSizes() const;
- /** Garbage collects non-context dependent data-structures.*/
+ /** Garbage collects non-context dependent data-structures. */
void garbageCollect();
- /** Return the RemoveITE's containsVisitor.*/
- theory::ContainsTermITEVistor* getContainsVisitor();
+ /** Return the RemoveITE's containsVisitor. */
+ theory::ContainsTermITEVisitor* getContainsVisitor();
private:
- theory::ContainsTermITEVistor* d_containsVisitor;
+ theory::ContainsTermITEVisitor* d_containsVisitor;
};/* class RemoveTTE */
bug522.smt2 \
bug528a.smt2 \
bug541.smt2 \
- bug544.smt2
+ bug544.smt2 \
+ bug548a.smt2
TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
--- /dev/null
+; COMMAND-LINE: --rewrite-divk --tlimit 1000
+; EXPECT: unknown
+(set-logic LIA)
+(declare-fun f (Int) Int)
+
+
+; instantiated version : cvc4 answers sat
+;(assert (= (f 1) (div 1 10)))
+;(assert (= (f 11) (div 11 10)))
+
+; cvc4 answers unsat, should be "sat", cvc4 expected to timeout or answer "unknown"
+(assert (forall ((x Int)) (= (f x) (div x 10))))
+
+(assert (= (f 1) 0))
+(assert (= (f 11) 1))
+
+(check-sat)
german73.smt2 \
PUZ001+1.smt2 \
refcount24.cvc.smt2 \
- bug0909.smt2
+ bug0909.smt2 \
+ fmf-bound-int.smt2
EXTRA_DIST = $(TESTS)
--- /dev/null
+; COMMAND-LINE: --finite-model-find --fmf-bound-int
+; EXPECT: sat
+(set-logic UFLIA)
+(declare-fun P (Int Int) Bool)
+(declare-fun Q (Int) Bool)
+(assert (forall ((x Int)) (=> (and (<= 0 x) (<= x (ite (P 0 0) 10 20))) (Q x))))
+(check-sat)
length_trick.smt2 length_trick2.smt2 length_gen_020.smt2 \
datatypes.smt2 datatypes_sat.smt2 set_A_new_fast_tableau-base.smt2 \
set_A_new_fast_tableau-base_sat.smt2 relation.smt2 simulate_rewriting.smt2 \
- reachability_back_to_the_future.smt2 native_arrays.smt2 reachability_bbttf_eT_arrays.smt2
+ reachability_back_to_the_future.smt2 native_arrays.smt2
+# reachability_bbttf_eT_arrays.smt2
EXTRA_DIST = $(TESTS)
fmf001.smt2 \
fmf002.smt2 \
type001.smt2 \
- type002.smt2 \
type003.smt2 \
model001.smt2 \
substr001.smt2 \
FAILING_TESTS =
-EXTRA_DIST = $(TESTS)
-
+EXTRA_DIST = $(TESTS) \
+ type002.smt2
# and make sure to distribute it
EXTRA_DIST +=
projects / cvc5.git / commitdiff