From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 11 Apr 2017 16:14:42 +0000 (-0500)
Subject: Bug fix in conjecture generation for --quant-ind.
X-Git-Tag: cvc5-1.0.0~5840
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e6e02c32c58f9e5edde2dd85fc7b19ef001eea03;p=cvc5.git

Bug fix in conjecture generation for --quant-ind.
---

diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 11adc61fd..a0c607e0e 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -356,6 +356,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
       eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
       while( !eqcs_i.isFinished() ){
         TNode r = (*eqcs_i);
+        Trace("sg-proc-debug") << "...eqc : " << r << std::endl;
         eqcs.push_back( r );
         if( r.getType().isBoolean() ){
           if( areEqual( r, getTermDatabase()->d_true ) ){
@@ -370,8 +371,10 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) {
         eq::EqClassIterator ieqc_i = eq::EqClassIterator( r, ee );
         while( !ieqc_i.isFinished() ){
           TNode n = (*ieqc_i);
+          Trace("sg-proc-debug") << "......term : " << n << std::endl;
           if( getTermDatabase()->hasTermCurrent( n ) ){
             if( isHandledTerm( n ) ){
+              getTermDatabase()->computeArgReps( n );
               d_op_arg_index[r].addTerm( getTermDatabase()->d_arg_reps[n], n );
             }
           }