Merge branch 'master' into fixParseOnlyfixParseOnly

20 files changed, 376 insertions, 33 deletions

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 1aa9a740f..03c464e08 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -7819,7 +7819,21 @@ void Solver::addSygusConstraint(const Term& term) const
       term.d_node->getType() == getNodeManager()->booleanType(), term)
       << "boolean term";
   //////// all checks before this line
-  d_smtEngine->assertSygusConstraint(*term.d_node);
+  d_smtEngine->assertSygusConstraint(*term.d_node, false);
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
+void Solver::addSygusAssume(const Term& term) const
+{
+  NodeManagerScope scope(getNodeManager());
+  CVC5_API_TRY_CATCH_BEGIN;
+  CVC5_API_SOLVER_CHECK_TERM(term);
+  CVC5_API_ARG_CHECK_EXPECTED(
+      term.d_node->getType() == getNodeManager()->booleanType(), term)
+      << "boolean term";
+  //////// all checks before this line
+  d_smtEngine->assertSygusConstraint(*term.d_node, true);
   ////////
   CVC5_API_TRY_CATCH_END;
 }
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 9324e4209..684b89114 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -4304,6 +4304,16 @@ class CVC5_EXPORT Solver
   void addSygusConstraint(const Term& term) const;
 
   /**
+   * Add a forumla to the set of Sygus assumptions.
+   * SyGuS v2:
+   * \verbatim
+   *   ( assume <term> )
+   * \endverbatim
+   * @param term the formula to add as an assumption
+   */
+  void addSygusAssume(const Term& term) const;
+
+  /**
    * Add a set of Sygus constraints to the current state that correspond to an
    * invariant synthesis problem.
    * SyGuS v2:
diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp
index 31a22b44a..fdb397d39 100644
--- a/src/expr/dtype.cpp
+++ b/src/expr/dtype.cpp
@@ -895,6 +895,19 @@ const std::vector<std::shared_ptr<DTypeConstructor> >& DType::getConstructors()
   return d_constructors;
 }
 
+std::unordered_set<TypeNode> DType::getSubfieldTypes() const
+{
+  std::unordered_set<TypeNode> subFieldTypes;
+  for (std::shared_ptr<DTypeConstructor> ctor : d_constructors)
+  {
+    for (size_t i = 0, nargs = ctor->getNumArgs(); i < nargs; i++)
+    {
+      subFieldTypes.insert(ctor->getArgType(i));
+    }
+  }
+  return subFieldTypes;
+}
+
 std::ostream& operator<<(std::ostream& os, const DType& dt)
 {
   // can only output datatypes in the cvc5 native language
diff --git a/src/expr/dtype.h b/src/expr/dtype.h
index a608b9adb..4f54f0af7 100644
--- a/src/expr/dtype.h
+++ b/src/expr/dtype.h
@@ -425,6 +425,12 @@ class DType
   const std::vector<std::shared_ptr<DTypeConstructor> >& getConstructors()
       const;
 
+  /**
+   * Return the subfield types of this datatype. This is the set of all types T
+   * for which there exists an argument to a constructor of type T.
+   */
+  std::unordered_set<TypeNode> getSubfieldTypes() const;
+
   /** prints this datatype to stream */
   void toStream(std::ostream& out) const;
 
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 22a042951..2c391169c 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -518,6 +518,7 @@ sygusCommand returns [std::unique_ptr<cvc5::Command> cmd]
   std::vector<std::pair<std::string, cvc5::api::Sort> > sortedVarNames;
   std::vector<cvc5::api::Term> sygusVars;
   std::string name;
+  bool isAssume;
   bool isInv;
   cvc5::api::Grammar* grammar = nullptr;
 }
@@ -568,14 +569,13 @@ sygusCommand returns [std::unique_ptr<cvc5::Command> cmd]
           new SynthFunCommand(name, fun, sygusVars, range, isInv, grammar));
     }
   | /* constraint */
-    CONSTRAINT_TOK {
+    ( CONSTRAINT_TOK { isAssume = false; } | ASSUME_TOK { isAssume = true; } )
+    {
       PARSER_STATE->checkThatLogicIsSet();
-      Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl;
-      Debug("parser-sygus") << "Sygus : read constraint..." << std::endl;
     }
     term[expr, expr2]
     { Debug("parser-sygus") << "...read constraint " << expr << std::endl;
-      cmd.reset(new SygusConstraintCommand(expr));
+      cmd.reset(new SygusConstraintCommand(expr, isAssume));
     }
   | /* inv-constraint */
     INV_CONSTRAINT_TOK
@@ -784,6 +784,11 @@ smt25Command[std::unique_ptr<cvc5::Command>* cmd]
     { PARSER_STATE->checkUserSymbol(name); }
     sortSymbol[t,CHECK_DECLARED]
     { // allow overloading here
+      if( PARSER_STATE->sygus() )
+      {
+        PARSER_STATE->parseErrorLogic("declare-const is not allowed in sygus "
+                                      "version 2.0");
+      }
       api::Term c =
           PARSER_STATE->bindVar(name, t, false, true);
       cmd->reset(new DeclareFunctionCommand(name, c, t)); }
@@ -2272,6 +2277,7 @@ SYNTH_INV_TOK : { PARSER_STATE->sygus()}?'synth-inv';
 CHECK_SYNTH_TOK : { PARSER_STATE->sygus()}?'check-synth';
 DECLARE_VAR_TOK : { PARSER_STATE->sygus()}?'declare-var';
 CONSTRAINT_TOK : { PARSER_STATE->sygus()}?'constraint';
+ASSUME_TOK : { PARSER_STATE->sygus()}?'assume';
 INV_CONSTRAINT_TOK : { PARSER_STATE->sygus()}?'inv-constraint';
 SET_FEATURE_TOK : { PARSER_STATE->sygus() }? 'set-feature';
 SYGUS_CONSTANT_TOK : { PARSER_STATE->sygus() }? 'Constant';
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index e038952c4..01fa7a9fd 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -204,6 +204,13 @@ void Printer::toStreamCmdDeclareFunction(std::ostream& out,
   printUnknownCommand(out, "declare-fun");
 }
 
+void Printer::toStreamCmdDeclareFunction(std::ostream& out, const Node& v) const
+{
+  std::stringstream vs;
+  vs << v;
+  toStreamCmdDeclareFunction(out, vs.str(), v.getType());
+}
+
 void Printer::toStreamCmdDeclarePool(std::ostream& out,
                                      const std::string& id,
                                      TypeNode type,
@@ -235,6 +242,25 @@ void Printer::toStreamCmdDefineFunction(std::ostream& out,
   printUnknownCommand(out, "define-fun");
 }
 
+void Printer::toStreamCmdDefineFunction(std::ostream& out,
+                                        Node v,
+                                        Node lambda) const
+{
+  std::stringstream vs;
+  vs << v;
+  std::vector<Node> formals;
+  Node body = lambda;
+  TypeNode rangeType = v.getType();
+  if (body.getKind() == kind::LAMBDA)
+  {
+    formals.insert(formals.end(), lambda[0].begin(), lambda[0].end());
+    body = lambda[1];
+    Assert(rangeType.isFunction());
+    rangeType = rangeType.getRangeType();
+  }
+  toStreamCmdDefineFunction(out, vs.str(), formals, rangeType, body);
+}
+
 void Printer::toStreamCmdDefineFunctionRec(
     std::ostream& out,
     const std::vector<Node>& funcs,
@@ -244,6 +270,32 @@ void Printer::toStreamCmdDefineFunctionRec(
   printUnknownCommand(out, "define-fun-rec");
 }
 
+void Printer::toStreamCmdDefineFunctionRec(
+    std::ostream& out,
+    const std::vector<Node>& funcs,
+    const std::vector<Node>& lambdas) const
+{
+  std::vector<std::vector<Node>> formals;
+  std::vector<Node> formulas;
+  for (const Node& l : lambdas)
+  {
+    std::vector<Node> formalsVec;
+    Node formula;
+    if (l.getKind() == kind::LAMBDA)
+    {
+      formalsVec.insert(formalsVec.end(), l[0].begin(), l[0].end());
+      formula = l[1];
+    }
+    else
+    {
+      formula = l;
+    }
+    formals.emplace_back(formalsVec);
+    formulas.emplace_back(formula);
+  }
+  toStreamCmdDefineFunctionRec(out, funcs, formals, formulas);
+}
+
 void Printer::toStreamCmdSetUserAttribute(std::ostream& out,
                                           const std::string& attr,
                                           Node n) const
@@ -288,6 +340,11 @@ void Printer::toStreamCmdConstraint(std::ostream& out, Node n) const
   printUnknownCommand(out, "constraint");
 }
 
+void Printer::toStreamCmdAssume(std::ostream& out, Node n) const
+{
+  printUnknownCommand(out, "assume");
+}
+
 void Printer::toStreamCmdInvConstraint(
     std::ostream& out, Node inv, Node pre, Node trans, Node post) const
 {
diff --git a/src/printer/printer.h b/src/printer/printer.h
index 5e141fe8f..499a9398f 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -87,6 +87,8 @@ class Printer
   virtual void toStreamCmdDeclareFunction(std::ostream& out,
                                           const std::string& id,
                                           TypeNode type) const;
+  /** Variant of above for a pre-existing variable */
+  void toStreamCmdDeclareFunction(std::ostream& out, const Node& v) const;
   /** Print declare-pool command */
   virtual void toStreamCmdDeclarePool(std::ostream& out,
                                       const std::string& id,
@@ -109,6 +111,8 @@ class Printer
                                          const std::vector<Node>& formals,
                                          TypeNode range,
                                          Node formula) const;
+  /** Variant of above that takes the definition */
+  void toStreamCmdDefineFunction(std::ostream& out, Node v, Node lambda) const;
 
   /** Print define-fun-rec command */
   virtual void toStreamCmdDefineFunctionRec(
@@ -116,6 +120,10 @@ class Printer
       const std::vector<Node>& funcs,
       const std::vector<std::vector<Node>>& formals,
       const std::vector<Node>& formulas) const;
+  /** Variant of above that takes the definition */
+  void toStreamCmdDefineFunctionRec(std::ostream& out,
+                                    const std::vector<Node>& funcs,
+                                    const std::vector<Node>& lambdas) const;
 
   /** Print set-user-attribute command */
   void toStreamCmdSetUserAttribute(std::ostream& out,
@@ -148,6 +156,9 @@ class Printer
   /** Print constraint command */
   virtual void toStreamCmdConstraint(std::ostream& out, Node n) const;
 
+  /** Print assume command */
+  virtual void toStreamCmdAssume(std::ostream& out, Node n) const;
+
   /** Print inv-constraint command */
   virtual void toStreamCmdInvConstraint(
       std::ostream& out, Node inv, Node pre, Node trans, Node post) const;
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 0d556c1dc..07c5b10d8 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1877,6 +1877,11 @@ void Smt2Printer::toStreamCmdConstraint(std::ostream& out, Node n) const
   out << "(constraint " << n << ')' << std::endl;
 }
 
+void Smt2Printer::toStreamCmdAssume(std::ostream& out, Node n) const
+{
+  out << "(assume " << n << ')' << std::endl;
+}
+
 void Smt2Printer::toStreamCmdInvConstraint(
     std::ostream& out, Node inv, Node pre, Node trans, Node post) const
 {
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index 729caebf4..fd7e0c7ac 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -124,6 +124,9 @@ class Smt2Printer : public cvc5::Printer
   /** Print constraint command */
   void toStreamCmdConstraint(std::ostream& out, Node n) const override;
 
+  /** Print assume command */
+  void toStreamCmdAssume(std::ostream& out, Node n) const override;
+
   /** Print inv-constraint command */
   void toStreamCmdInvConstraint(std::ostream& out,
                                 Node inv,
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 522c38040..4b04abcb2 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -732,7 +732,9 @@ void SynthFunCommand::toStream(std::ostream& out,
 /* class SygusConstraintCommand */
 /* -------------------------------------------------------------------------- */
 
-SygusConstraintCommand::SygusConstraintCommand(const api::Term& t) : d_term(t)
+SygusConstraintCommand::SygusConstraintCommand(const api::Term& t,
+                                               bool isAssume)
+    : d_term(t), d_isAssume(isAssume)
 {
 }
 
@@ -740,7 +742,14 @@ void SygusConstraintCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
-    solver->addSygusConstraint(d_term);
+    if (d_isAssume)
+    {
+      solver->addSygusAssume(d_term);
+    }
+    else
+    {
+      solver->addSygusConstraint(d_term);
+    }
     d_commandStatus = CommandSuccess::instance();
   }
   catch (exception& e)
@@ -753,12 +762,12 @@ api::Term SygusConstraintCommand::getTerm() const { return d_term; }
 
 Command* SygusConstraintCommand::clone() const
 {
-  return new SygusConstraintCommand(d_term);
+  return new SygusConstraintCommand(d_term, d_isAssume);
 }
 
 std::string SygusConstraintCommand::getCommandName() const
 {
-  return "constraint";
+  return d_isAssume ? "assume" : "constraint";
 }
 
 void SygusConstraintCommand::toStream(std::ostream& out,
@@ -766,7 +775,15 @@ void SygusConstraintCommand::toStream(std::ostream& out,
                                       size_t dag,
                                       Language language) const
 {
-  Printer::getPrinter(language)->toStreamCmdConstraint(out, termToNode(d_term));
+  if (d_isAssume)
+  {
+    Printer::getPrinter(language)->toStreamCmdAssume(out, termToNode(d_term));
+  }
+  else
+  {
+    Printer::getPrinter(language)->toStreamCmdConstraint(out,
+                                                         termToNode(d_term));
+  }
 }
 
 /* -------------------------------------------------------------------------- */
@@ -1186,8 +1203,8 @@ void DeclareFunctionCommand::toStream(std::ostream& out,
                                       size_t dag,
                                       Language language) const
 {
-  Printer::getPrinter(language)->toStreamCmdDeclareFunction(
-      out, d_func.toString(), sortToTypeNode(d_sort));
+  Printer::getPrinter(language)->toStreamCmdDeclareFunction(out,
+                                                            termToNode(d_func));
 }
 
 /* -------------------------------------------------------------------------- */
diff --git a/src/smt/command.h b/src/smt/command.h
index b374a48c9..7587aaa63 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -765,7 +765,7 @@ class CVC5_EXPORT SynthFunCommand : public DeclarationDefinitionCommand
 class CVC5_EXPORT SygusConstraintCommand : public Command
 {
  public:
-  SygusConstraintCommand(const api::Term& t);
+  SygusConstraintCommand(const api::Term& t, bool isAssume = false);
   /** returns the declared constraint */
   api::Term getTerm() const;
   /** invokes this command
@@ -787,6 +787,8 @@ class CVC5_EXPORT SygusConstraintCommand : public Command
  protected:
   /** the declared constraint */
   api::Term d_term;
+  /** true if this is a sygus assumption */
+  bool d_isAssume;
 };
 
 /** Declares a sygus invariant constraint
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 279761b43..46e83e9e7 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -994,11 +994,11 @@ void SmtEngine::declareSynthFun(Node func,
   declareSynthFun(func, sygusType, isInv, vars);
 }
 
-void SmtEngine::assertSygusConstraint(Node constraint)
+void SmtEngine::assertSygusConstraint(Node n, bool isAssume)
 {
   SmtScope smts(this);
   finishInit();
-  d_sygusSolver->assertSygusConstraint(constraint);
+  d_sygusSolver->assertSygusConstraint(n, isAssume);
 }
 
 void SmtEngine::assertSygusInvConstraint(Node inv,
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 06a1c9ae4..9f17fa27e 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -416,8 +416,12 @@ class CVC5_EXPORT SmtEngine
    */
   void declareSynthFun(Node func, bool isInv, const std::vector<Node>& vars);
 
-  /** Add a regular sygus constraint.*/
-  void assertSygusConstraint(Node constraint);
+  /**
+   * Add a regular sygus constraint or assumption.
+   * @param n The formula
+   * @param isAssume True if n is an assumption.
+   */
+  void assertSygusConstraint(Node n, bool isAssume = false);
 
   /**
    * Add an invariant constraint.
diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp
index 32a0ee220..ff701ec48 100644
--- a/src/smt/sygus_solver.cpp
+++ b/src/smt/sygus_solver.cpp
@@ -90,10 +90,18 @@ void SygusSolver::declareSynthFun(Node fn,
   setSygusConjectureStale();
 }
 
-void SygusSolver::assertSygusConstraint(Node constraint)
+void SygusSolver::assertSygusConstraint(Node n, bool isAssume)
 {
-  Trace("smt") << "SygusSolver::assertSygusConstrant: " << constraint << "\n";
-  d_sygusConstraints.push_back(constraint);
+  Trace("smt") << "SygusSolver::assertSygusConstrant: " << n
+               << ", isAssume=" << isAssume << "\n";
+  if (isAssume)
+  {
+    d_sygusAssumps.push_back(n);
+  }
+  else
+  {
+    d_sygusConstraints.push_back(n);
+  }
 
   // sygus conjecture is now stale
   setSygusConjectureStale();
@@ -186,13 +194,14 @@ Result SygusSolver::checkSynth(Assertions& as)
     NodeManager* nm = NodeManager::currentNM();
     // build synthesis conjecture from asserted constraints and declared
     // variables/functions
-    std::vector<Node> bodyv;
     Trace("smt") << "Sygus : Constructing sygus constraint...\n";
-    size_t nconstraints = d_sygusConstraints.size();
-    Node body = nconstraints == 0
-                    ? nm->mkConst(true)
-                    : (nconstraints == 1 ? d_sygusConstraints[0]
-                                         : nm->mkNode(AND, d_sygusConstraints));
+    Node body = nm->mkAnd(d_sygusConstraints);
+    // note that if there are no constraints, then assumptions are irrelevant
+    if (!d_sygusConstraints.empty() && !d_sygusAssumps.empty())
+    {
+      Node bodyAssump = nm->mkAnd(d_sygusAssumps);
+      body = nm->mkNode(IMPLIES, bodyAssump, body);
+    }
     body = body.notNode();
     Trace("smt") << "...constructed sygus constraint " << body << std::endl;
     if (!d_sygusVars.empty())
diff --git a/src/smt/sygus_solver.h b/src/smt/sygus_solver.h
index 3db615037..90a6a87f0 100644
--- a/src/smt/sygus_solver.h
+++ b/src/smt/sygus_solver.h
@@ -82,8 +82,8 @@ class SygusSolver
                        bool isInv,
                        const std::vector<Node>& vars);
 
-  /** Add a regular sygus constraint.*/
-  void assertSygusConstraint(Node constraint);
+  /** Add a regular sygus constraint or assumption.*/
+  void assertSygusConstraint(Node n, bool isAssume);
 
   /**
    * Add an invariant constraint.
@@ -185,6 +185,8 @@ class SygusSolver
   std::vector<Node> d_sygusVars;
   /** sygus constraints */
   std::vector<Node> d_sygusConstraints;
+  /** sygus assumptions */
+  std::vector<Node> d_sygusAssumps;
   /** functions-to-synthesize */
   std::vector<Node> d_sygusFunSymbols;
   /**
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index fd734b321..90ad99e70 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1241,6 +1241,7 @@ set(regress_0_tests
   regress0/strings/unicode-esc.smt2
   regress0/strings/unsound-0908.smt2
   regress0/strings/unsound-repl-rewrite.smt2
+  regress0/sygus/assume-simple.sy
   regress0/sygus/array-grammar-select.sy
   regress0/sygus/ccp16.lus.sy
   regress0/sygus/cegqi-si-string-triv-2fun.sy
@@ -2398,6 +2399,7 @@ set(regress_1_tests
   regress1/sygus/re-concat.sy
   regress1/sygus/repair-const-rl.sy
   regress1/sygus/replicate-mod.sy
+  regress1/sygus/replicate-mod-assume.sy
   regress1/sygus/rex-strings-alarm.sy
   regress1/sygus/sets-pred-test.sy
   regress1/sygus/simple-regexp.sy
diff --git a/test/regress/regress0/sygus/assume-simple.sy b/test/regress/regress0/sygus/assume-simple.sy
new file mode 100644
index 000000000..58f3753d8
--- /dev/null
+++ b/test/regress/regress0/sygus/assume-simple.sy
@@ -0,0 +1,13 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+
+(set-logic LIA)
+(synth-fun f ((x Int)) Int
+  ((Start Int))
+  ((Start Int (x 0 1 (+ Start Start)))))
+(declare-var y Int)
+(assume (>= y 0))
+(constraint (>= (f y) 0))
+(constraint (>= (f y) y))
+; lambda x. x is a valid solution
+(check-synth)
diff --git a/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy b/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy
index 6a149cc71..cf8e4da31 100644
--- a/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy
+++ b/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy
@@ -1,6 +1,6 @@
 ; REQUIRES: no-competition
 ; COMMAND-LINE: --sygus-out=status --sygus-rec-fun --lang=sygus2
-; EXPECT-ERROR: (error "Parse Error: pLTL-sygus-syntax-err.sy:80.19: number of arguments does not match the constructor type
+; EXPECT-ERROR: (error "Parse Error: pLTL-sygus-syntax-err.sy:78.19: number of arguments does not match the constructor type
 ; EXPECT-ERROR:
 ; EXPECT-ERROR: (Op2 <O2> <F>)
 ; EXPECT-ERROR: ^
@@ -31,8 +31,6 @@
 )
 
 ; Trace Length.
-(declare-const tn Int)
-(assert (= tn 2))
 
 ;cTrace Declaration (trace_index, variable_index)
 (define-fun val ((i Int) (x Var)) Bool
@@ -44,7 +42,7 @@
 
 ;cpLTL Semantics
 (define-fun-rec holds ((f Formula) (t Time)) Bool
-  (and (<= 0 t tn)
+  (and (<= 0 t 2)
        (match f (
          ((P i) (val t i))
 
@@ -54,7 +52,7 @@
 
              (Y (and (< 0 t) (holds g (- t 1))))
 
-             (G (and (holds g t) (or (= t tn) (holds f (+ t 1)))))
+             (G (and (holds g t) (or (= t 2) (holds f (+ t 1)))))
 
              (H (and (holds g t) (or (= t 0) (holds f (- t 1)))))
           )))
diff --git a/test/regress/regress1/sygus/replicate-mod-assume.sy b/test/regress/regress1/sygus/replicate-mod-assume.sy
new file mode 100644
index 000000000..c10cab2f5
--- /dev/null
+++ b/test/regress/regress1/sygus/replicate-mod-assume.sy
@@ -0,0 +1,157 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic LIA)
+(synth-fun fr0 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr1 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr10 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr11 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr12 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr13 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr14 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr15 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr16 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr17 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr18 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr19 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr2 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr20 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr21 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr22 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr23 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr24 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr25 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr26 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr27 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr28 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr29 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr3 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr30 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr31 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr32 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr33 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr34 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr35 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr36 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr4 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr5 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr6 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr7 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr8 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun fr9 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m0 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m1 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m10 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m11 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m12 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m13 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m14 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m15 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m16 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m17 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m2 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m3 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m4 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m5 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m6 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m7 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m8 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun m9 ((_v Int) (n Int) (x Int)) Int
+       )
+(synth-fun p0 ((_v Int) (n Int) (x Int)) Int)
+(synth-fun p1 ((_v Int) (n Int) (x Int)) Int)
+(synth-fun p2 ((_v Int) (n Int) (x Int)) Int)
+(synth-fun p3 ((_v Int) (n Int) (x Int)) Int)
+(synth-fun p4 ((_v Int) (n Int) (x Int)) Int)
+(synth-fun p5 ((_v Int) (n Int) (x Int)) Int)
+(declare-var n Int)
+(declare-var x Int)
+(declare-var x10 Int)
+(declare-var x11 Int)
+(declare-var x14 Int)
+(declare-var x15 Int)
+(declare-var x2 Int)
+(declare-var x3 Int)
+(declare-var x6 Int)
+(declare-var x7 Int)
+(declare-var _v Int)
+(assume (and (= false (<= n 0)) (>= n 0)))
+(constraint (>= (p4 _v n x) 0))
+(constraint (and (and (and (>= (m6 _v n x) 0) (>= (m8 _v n x) 0)) (>= (m9 _v n x) 0)) (= (m6 _v n x) (+ (m8 _v n x) (m9 _v n x)))))
+(constraint (and (and (and (>= (fr17 _v n x) 0) (>= (fr19 _v n x) 0)) (>= (fr20 _v n x) 0)) (= (fr17 _v n x) (+ (fr19 _v n x) (fr20 _v n x)))))
+(constraint (and (and (and (>= (fr15 _v n x) 0) (>= (fr17 _v n x) 0)) (>= (fr18 _v n x) 0)) (= (fr15 _v n x) (+ (fr17 _v n x) (fr18 _v n x)))))
+(constraint (and (and (and (>= (m1 _v n x) 0) (>= (m6 _v n x) 0)) (>= (m7 _v n x) 0)) (= (m1 _v n x) (+ (m6 _v n x) (m7 _v n x)))))
+(constraint (and (and (and (>= (fr13 _v n x) 0) (>= (fr15 _v n x) 0)) (>= (fr16 _v n x) 0)) (= (fr13 _v n x) (+ (fr15 _v n x) (fr16 _v n x)))))
+(constraint (and (and (and (>= (fr12 _v n x) 0) (>= (fr13 _v n x) 0)) (>= (fr14 _v n x) 0)) (= (fr12 _v n x) (+ (fr13 _v n x) (fr14 _v n x)))))
+(constraint (and (and (and (and (and (and (= (+ (+ (+ 0 (p1 _v n x)) (fr1 _v n x)) 0) (+ (+ (+ 0 0) (fr12 _v n x)) 0)) (>= (fr1 _v n x) 0)) (>= (fr12 _v n x) 0)) (>= 0 0)) (>= 0 0)) (>= 0 0)) (>= 0 0)))
+(constraint (=> (and (and (= false (<= n 0)) (= _v x)) (>= n 0)) (>= 0 (+ (p4 _v n x) (- (+ (fr18 _v n x) 0))))))
+(constraint (>= 0 (- (+ (fr14 _v n x) 0))))
+(constraint (>= (p5 _v n x) (p4 _v n x)))
+(constraint (>= (p5 _v n x) 0))
+(constraint (and (and (and (>= (m10 _v n x) 0) (>= (m12 _v n x) 0)) (>= (m13 _v n x) 0)) (= (m10 _v n x) (+ (m12 _v n x) (m13 _v n x)))))
+(constraint (and (and (and (>= (fr25 _v n x) 0) (>= (fr27 _v n x) 0)) (>= (fr28 _v n x) 0)) (= (fr25 _v n x) (+ (fr27 _v n x) (fr28 _v n x)))))
+(constraint (and (and (and (>= (fr23 _v n x) 0) (>= (fr25 _v n x) 0)) (>= (fr26 _v n x) 0)) (= (fr23 _v n x) (+ (fr25 _v n x) (fr26 _v n x)))))
+(constraint (and (and (and (>= (m7 _v n x) 0) (>= (m10 _v n x) 0)) (>= (m11 _v n x) 0)) (= (m7 _v n x) (+ (m10 _v n x) (m11 _v n x)))))
+(constraint (and (and (and (>= (fr21 _v n x) 0) (>= (fr23 _v n x) 0)) (>= (fr24 _v n x) 0)) (= (fr21 _v n x) (+ (fr23 _v n x) (fr24 _v n x)))))
+(constraint (and (and (and (>= (- (fr16 _v n x) 1) 0) (>= (fr21 _v n x) 0)) (>= (fr22 _v n x) 0)) (= (- (fr16 _v n x) 1) (+ (fr21 _v n x) (fr22 _v n x)))))
+(constraint (=> false (>= 0 (- (+ (fr26 _v n x) 0)))))
+(constraint (and (and (and (>= (m14 _v n x) 0) (>= (m16 _v n x) 0)) (>= (m17 _v n x) 0)) (= (m14 _v n x) (+ (m16 _v n x) (m17 _v n x)))))
+(constraint (and (and (and (>= (fr33 _v n x) 0) (>= (fr35 _v n x) 0)) (>= (fr36 _v n x) 0)) (= (fr33 _v n x) (+ (fr35 _v n x) (fr36 _v n x)))))
+(constraint (and (and (and (>= (fr31 _v n x) 0) (>= (fr33 _v n x) 0)) (>= (fr34 _v n x) 0)) (= (fr31 _v n x) (+ (fr33 _v n x) (fr34 _v n x)))))
+(constraint (and (and (and (>= (m13 _v n x) 0) (>= (m14 _v n x) 0)) (>= (m15 _v n x) 0)) (= (m13 _v n x) (+ (m14 _v n x) (m15 _v n x)))))
+(constraint (and (and (and (>= (fr29 _v n x) 0) (>= (fr31 _v n x) 0)) (>= (fr32 _v n x) 0)) (= (fr29 _v n x) (+ (fr31 _v n x) (fr32 _v n x)))))
+(constraint (and (and (and (>= (fr28 _v n x) 0) (>= (fr29 _v n x) 0)) (>= (fr30 _v n x) 0)) (= (fr28 _v n x) (+ (fr29 _v n x) (fr30 _v n x)))))
+(check-synth)
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index 1f6f7801e..9042209e2 100644
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -2300,6 +2300,20 @@ TEST_F(TestApiBlackSolver, addSygusConstraint)
   ASSERT_THROW(slv.addSygusConstraint(boolTerm), CVC5ApiException);
 }
 
+TEST_F(TestApiBlackSolver, addSygusAssume)
+{
+  Term nullTerm;
+  Term boolTerm = d_solver.mkBoolean(false);
+  Term intTerm = d_solver.mkInteger(1);
+
+  ASSERT_NO_THROW(d_solver.addSygusAssume(boolTerm));
+  ASSERT_THROW(d_solver.addSygusAssume(nullTerm), CVC5ApiException);
+  ASSERT_THROW(d_solver.addSygusAssume(intTerm), CVC5ApiException);
+
+  Solver slv;
+  ASSERT_THROW(slv.addSygusAssume(boolTerm), CVC5ApiException);
+}
+
 TEST_F(TestApiBlackSolver, addSygusInvConstraint)
 {
   Sort boolean = d_solver.getBooleanSort();