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.

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index c0484e52b0a2b41cade002d828ae81cae2444fa9..d1fbfe9692c2514a7b10cf7e1e74006e6dfe641e 100644 (file)
--- 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 b82b958aff392a3fb689478dd7eccae9799003d2..bccb33f1dc91c0fce7a7df4f5d005054fba29e80 100644 (file)
--- 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 83d9ac48cb538b48884e6ebe01703a3f2f7dc39d..47290467d95ee8c9c59fa62e3310d6d1f89d79ec 100644 (file)
--- 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 (file)
index 0000000..c9d4eb0
--- /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)