From ac5ef49e14154daee4200783b57584febb726a4e Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 11 Mar 2020 12:18:59 -0500
Subject: [PATCH] Fix non-parametrized operators in subgoal generation (#4023)

Fixes #4021.

We were previously constructing a malformed HO_APPLY as part of a subgoal for induction.
---
 src/parser/smt2/smt2.cpp                           |  1 -
 src/theory/quantifiers/conjecture_generator.cpp    | 10 ++++++----
 test/regress/CMakeLists.txt                        |  1 +
 .../regress1/quantifiers/issue4021-ind-opts.smt2   | 14 ++++++++++++++
 4 files changed, 21 insertions(+), 5 deletions(-)
 create mode 100644 test/regress/regress1/quantifiers/issue4021-ind-opts.smt2

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index c0484e52b..d1fbfe969 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1841,7 +1841,6 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
   }
   else if (isBuiltinOperator)
   {
-    Trace("ajr-temp") << "mkTerm builtin operator" << std::endl;
     if (!opts.getUfHo() && (kind == api::EQUAL || kind == api::DISTINCT))
     {
       // need --uf-ho if these operators are applied over function args
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index b82b958af..bccb33f1d 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -66,12 +66,14 @@ Node OpArgIndex::getGroundTerm( ConjectureGenerator * s, std::vector< TNode >& a
       }
     }
     return Node::null();
-  }else{
-    std::vector< TNode > args2;
+  }
+  std::vector<TNode> args2;
+  if (d_op_terms[0].getMetaKind() == kind::metakind::PARAMETERIZED)
+  {
     args2.push_back( d_ops[0] );
-    args2.insert( args2.end(), args.begin(), args.end() );
-    return NodeManager::currentNM()->mkNode( d_op_terms[0].getKind(), args2 );
   }
+  args2.insert(args2.end(), args.begin(), args.end());
+  return NodeManager::currentNM()->mkNode(d_op_terms[0].getKind(), args2);
 }
 
 void OpArgIndex::getGroundTerms( ConjectureGenerator * s, std::vector< TNode >& terms ) {
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 83d9ac48c..47290467d 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1490,6 +1490,7 @@ set(regress_1_tests
   regress1/quantifiers/issue3724-quant.smt2
   regress1/quantifiers/issue3765.smt2
   regress1/quantifiers/issue3765-quant-dd.smt2
+  regress1/quantifiers/issue4021-ind-opts.smt2
   regress1/quantifiers/issue993.smt2
   regress1/quantifiers/javafe.ast.StmtVec.009.smt2
   regress1/quantifiers/lra-vts-inf.smt2
diff --git a/test/regress/regress1/quantifiers/issue4021-ind-opts.smt2 b/test/regress/regress1/quantifiers/issue4021-ind-opts.smt2
new file mode 100644
index 000000000..c9d4eb034
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue4021-ind-opts.smt2
@@ -0,0 +1,14 @@
+(set-logic ALL)
+(set-option :ag-miniscope-quant true)
+(set-option :conjecture-gen true)
+(set-option :int-wf-ind true)
+(set-option :quant-model-ee true)
+(set-option :sygus-inference true)
+(set-option :uf-ho true)
+(set-info :status unsat)
+(declare-fun a () Real)
+(declare-fun b () Real)
+(declare-fun c () Real)
+(declare-fun e () Real)
+(assert (forall ((d Real)) (and (or (< (/ (* (- a) d) 0) c) (> b 0.0)) (= (= d 0) (= e 0)))))
+(check-sat)
-- 
2.30.2