From e6e02c32c58f9e5edde2dd85fc7b19ef001eea03 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 11 Apr 2017 11:14:42 -0500
Subject: [PATCH] Bug fix in conjecture generation for --quant-ind.

---
 src/theory/quantifiers/conjecture_generator.cpp | 3 +++
 1 file changed, 3 insertions(+)

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 );
             }
           }
-- 
2.30.2