Make Sygus conjectures higher-order (#1244)

* Represent sygus synthesis conjectures using higher-order quantification, remove associated hacks.

* Minor fix

* Fix bug in Node::hasBoundVar for non-ground operators.

* Add regression.

* Address review.

* Apply clang format.

12 files changed, 187 insertions, 30 deletions

diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 75e37151a..126feadd8 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -111,6 +111,9 @@ bool NodeTemplate<ref_count>::hasBoundVar() {
         hasBv = (*i).hasBoundVar();
       }
     }
+    if (!hasBv && hasOperator()) {
+      hasBv = getOperator().hasBoundVar();
+    }
     setAttribute(HasBoundVarAttr(), hasBv);
     setAttribute(HasBoundVarComputedAttr(), true);
     Debug("bva") << *this << " has bva : " << getAttribute(HasBoundVarAttr()) << std::endl;
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 05faf040e..4d39c7635 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -626,6 +626,7 @@ sygusCommand [std::unique_ptr<CVC4::Command>* cmd]
       synth_fun = PARSER_STATE->mkBoundVar(fun, synth_fun_type);
       // we add a declare function command here
       // this is the single unmuted command in the sequence generated by this smt2 command
+      // TODO (as part of #1170) : make this a standard command.
       seq->addCommand(new DeclareFunctionCommand(fun, synth_fun, synth_fun_type));
       PARSER_STATE->pushScope(true);
       for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index bc9f2a06f..0fc3678c7 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1081,13 +1081,17 @@ const void Smt2::getSygusPrimedVars( std::vector<Expr>& vars, bool isPrimed ) {
 }
 
 const void Smt2::addSygusFunSymbol( Type t, Expr synth_fun ){
-  //FIXME #1205 : we should not create a proxy, instead quantify on synth_fun and set Type t as an attribute
+  // When constructing the synthesis conjecture, we quantify on the
+  // (higher-order) bound variable synth_fun.
+  d_sygusFunSymbols.push_back(synth_fun);
+
+  // Variable "sfproxy" carries the type, which may be a SyGuS datatype
+  // that corresponds to syntactic restrictions.
   Expr sym = mkBoundVar("sfproxy", t);
-  d_sygusFunSymbols.push_back(sym);
-  
   std::vector< Expr > attr_value;
-  attr_value.push_back( synth_fun );
-  Command* cattr = new SetUserAttributeCommand("sygus-synth-fun", sym, attr_value);
+  attr_value.push_back(sym);
+  Command* cattr =
+      new SetUserAttributeCommand("sygus-synth-grammar", synth_fun, attr_value);
   cattr->setMuted(true);
   preemptCommand(cattr);
 }
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 4bcb78867..e32d8913d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -4574,12 +4574,7 @@ Result SmtEngine::checkSynth(const Expr& e) throw(Exception) {
       Trace("smt-synth") << "Compute single invocation for " << conj_se << "..." << std::endl;
       quantifiers::SingleInvocationPartition sip;
       std::vector< Node > funcs;
-      for( unsigned i=0; i<conj[0].getNumChildren(); i++ ){
-        // TODO : revisit this when addressing #1205
-        Node sf = conj[0][i].getAttribute(theory::SygusSynthFunAttribute());
-        Assert( !sf.isNull() );
-        funcs.push_back( sf );
-      }
+      funcs.insert(funcs.end(), conj[0].begin(), conj[0].end());
       sip.init( funcs, conj_se );
       Trace("smt-synth") << "...finished, got:" << std::endl;
       sip.debugPrint("smt-synth");
diff --git a/src/theory/quantifiers/ce_guided_conjecture.cpp b/src/theory/quantifiers/ce_guided_conjecture.cpp
index a838a6a0c..a380dcbf2 100644
--- a/src/theory/quantifiers/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/ce_guided_conjecture.cpp
@@ -72,11 +72,10 @@ void CegConjecture::assign( Node q ) {
     // carry the templates
     for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
       Node v = q[0][i];
-      Node sf = v.getAttribute(SygusSynthFunAttribute());
-      Node templ = d_ceg_si->getTemplate(sf);
+      Node templ = d_ceg_si->getTemplate(v);
       if( !templ.isNull() ){
-        templates[sf] = templ;
-        templates_arg[sf] = d_ceg_si->getTemplateArg(sf);
+        templates[v] = templ;
+        templates_arg[v] = d_ceg_si->getTemplateArg(v);
       }
     }
   }
@@ -562,7 +561,7 @@ void CegConjecture::printSynthSolution( std::ostream& out, bool singleInvocation
         status = 1;
         
         //check if there was a template
-        Node sf = d_quant[0][i].getAttribute(SygusSynthFunAttribute());
+        Node sf = d_quant[0][i];
         Node templ = d_ceg_si->getTemplate( sf );
         if( !templ.isNull() ){
           Trace("cegqi-inv-debug") << sf << " used template : " << templ << std::endl;
diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index bf09c83f7..3349492a2 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -126,8 +126,7 @@ void CegConjectureSingleInv::initialize( Node q ) {
   std::vector< Node > progs;
   std::map< Node, std::vector< Node > > prog_vars;
   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-    Node v = q[0][i];
-    Node sf = v.getAttribute(SygusSynthFunAttribute());
+    Node sf = q[0][i];
     progs.push_back( sf );
     Node sfvl = sf.getAttribute(SygusSynthFunVarListAttribute());
     for( unsigned j=0; j<sfvl.getNumChildren(); j++ ){
@@ -469,7 +468,7 @@ Node CegConjectureSingleInv::getSolution( unsigned sol_index, TypeNode stn, int&
   Assert( !d_lemmas_produced.empty() );
   const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
   Node varList = Node::fromExpr( dt.getSygusVarList() );
-  Node prog = d_quant[0][sol_index].getAttribute(SygusSynthFunAttribute());
+  Node prog = d_quant[0][sol_index];
   std::vector< Node > vars;
   Node s;
   if( d_prog_to_sol_index.find( prog )==d_prog_to_sol_index.end() ){
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index ac3fb85d1..c9a7f07ab 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -51,11 +51,12 @@ void QuantAttributes::setUserAttribute( const std::string& attr, Node n, std::ve
     Trace("quant-attr-debug") << "Set sygus " << n << std::endl;
     SygusAttribute ca;
     n.setAttribute( ca, true );
-  }else if( attr=="sygus-synth-fun" ){
+  } else if (attr == "sygus-synth-grammar") {
     Assert( node_values.size()==1 );
-    Trace("quant-attr-debug") << "Set sygus synth fun " << n << " to "  << node_values[0] << std::endl;
-    SygusSynthFunAttribute ssfa;
-    n.setAttribute( ssfa, node_values[0] );
+    Trace("quant-attr-debug") << "Set sygus synth grammar " << n << " to "
+                              << node_values[0] << std::endl;
+    SygusSynthGrammarAttribute ssg;
+    n.setAttribute(ssg, node_values[0]);
   }else if( attr=="sygus-synth-fun-var-list" ){
     Assert( node_values.size()==1 );
     Trace("quant-attr-debug") << "Set sygus synth fun var list to " << n << " to "  << node_values[0] << std::endl;
diff --git a/src/theory/quantifiers/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus_grammar_cons.cpp
index 2eb541e66..6152417a5 100644
--- a/src/theory/quantifiers/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus_grammar_cons.cpp
@@ -83,9 +83,11 @@ Node CegGrammarConstructor::process( Node q, std::map< Node, Node >& templates,
   std::vector< Node > ebvl;
   Node qbody_subs = q[1];
   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
-    Node v = q[0][i];
-    Node sf = v.getAttribute(SygusSynthFunAttribute());
-    Assert( !sf.isNull() );
+    Node sf = q[0][i];
+    // v encodes the syntactic restrictions (via an inductive datatype) on sf
+    // from the input
+    Node v = sf.getAttribute(SygusSynthGrammarAttribute());
+    Assert(!v.isNull());
     Node sfvl = sf.getAttribute(SygusSynthFunVarListAttribute());
     // sfvl may be null for constant synthesis functions
     Trace("cegqi-debug") << "...sygus var list associated with " << sf << " is " << sfvl << std::endl;
diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h
index 2360c5bfb..a0b3b8ec2 100644
--- a/src/theory/quantifiers/term_util.h
+++ b/src/theory/quantifiers/term_util.h
@@ -73,8 +73,9 @@ struct SygusProxyAttributeId {};
 typedef expr::Attribute<SygusProxyAttributeId, Node> SygusProxyAttribute;
 
 // attribute for associating a synthesis function with a first order variable
-struct SygusSynthFunAttributeId {};
-typedef expr::Attribute<SygusSynthFunAttributeId, Node> SygusSynthFunAttribute;
+struct SygusSynthGrammarAttributeId {};
+typedef expr::Attribute<SygusSynthGrammarAttributeId, Node>
+    SygusSynthGrammarAttribute;
 
 // attribute for associating a variable list with a synth fun
 struct SygusSynthFunVarListAttributeId {};
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 855cdb911..66e05b1cd 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -44,7 +44,7 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, Output
   out.handleUserAttribute( "conjecture", this );
   out.handleUserAttribute( "fun-def", this );
   out.handleUserAttribute( "sygus", this );
-  out.handleUserAttribute( "sygus-synth-fun", this );
+  out.handleUserAttribute("sygus-synth-grammar", this);
   out.handleUserAttribute( "sygus-synth-fun-var-list", this );
   out.handleUserAttribute( "synthesis", this );
   out.handleUserAttribute( "quant-inst-max-level", this );
diff --git a/test/regress/regress1/sygus/MPwL_d1s3.sy b/test/regress/regress1/sygus/MPwL_d1s3.sy
new file mode 100644
index 000000000..b5b848848
--- /dev/null
+++ b/test/regress/regress1/sygus/MPwL_d1s3.sy
@@ -0,0 +1,151 @@
+; EXPECT: unsat
+; COMMAND-LINE: --no-dump-synth 
+(set-logic LIA)
+
+(define-fun get-y ((currPoint Int)) Int 
+(ite (< currPoint 10) 0 (ite (< currPoint 20) 1 (ite (< currPoint 30) 2 (ite (< currPoint 40) 3 (ite (< currPoint 50) 4 (ite (< currPoint 60) 5 (ite (< currPoint 70) 6 (ite (< currPoint 80) 7 (ite (< currPoint 90) 8 9))))))))))
+
+(define-fun get-x ((currPoint Int)) Int
+	(- currPoint (* (get-y currPoint) 10)))
+(define-fun interpret-move (( currPoint Int ) ( move Int)) Int
+(ite (= move 0) currPoint 
+(ite (= move 1)  (ite (or (< (+ (get-y currPoint) 1) 0) (>= (+ (get-y currPoint) 1) 10))     currPoint (+ currPoint  10)) 
+(ite (= move 2)  (ite (or (< (+ (get-x currPoint) 1) 0) (>= (+ (get-x currPoint) 1) 10))     currPoint (+ currPoint  1)) 
+(ite (= move 3)  (ite (or (< (+ (get-y currPoint) -1) 0) (>= (+ (get-y currPoint) -1) 10))     currPoint (+ currPoint  -10)) 
+(ite (= move 4)  (ite (or (< (+ (get-x currPoint) -1) 0) (>= (+ (get-x currPoint) -1) 10))     currPoint (+ currPoint  -1)) 
+currPoint))))))
+
+(define-fun interpret-move-obstacle-0 (( currPoint Int ) ( move Int)) Int
+(ite (= move 0)  (ite (or (< (+ (get-y currPoint) 1) 0) (>= (+ (get-y currPoint) 1) 10))     currPoint (+ currPoint  10)) 
+(ite (= move 1)  (ite (or (< (+ (get-y currPoint) -1) 0) (>= (+ (get-y currPoint) -1) 10))     currPoint (+ currPoint  -10)) 
+currPoint)))
+
+(define-fun interpret-move-obstacle-1 (( currPoint Int ) ( move Int)) Int
+(ite (= move 0)  (ite (or (< (+ (get-y currPoint) 1) 0) (>= (+ (get-y currPoint) 1) 10))     currPoint (+ currPoint  10)) 
+(ite (= move 1) currPoint 
+(ite (= move 2)  (ite (or (< (+ (get-y currPoint) -1) 0) (>= (+ (get-y currPoint) -1) 10))     currPoint (+ currPoint  -10)) 
+currPoint))))
+
+(define-fun allowable-move-obstacle-0 (( start Int ) ( end Int)) Bool
+	(or (= (interpret-move-obstacle-0 start 0) end)
+	(or (= (interpret-move-obstacle-0 start 1) end) false)))
+
+(define-fun allowable-move-obstacle-1 (( start Int ) ( end Int)) Bool
+	(or (= (interpret-move-obstacle-1 start 0) end)
+	(or (= (interpret-move-obstacle-1 start 1) end)
+	(or (= (interpret-move-obstacle-1 start 2) end) false))))
+
+(define-fun get-move-obstacle-0 (( start Int ) ( end Int)) Int
+	(ite (= (interpret-move-obstacle-0 start 0) end) 0 
+	(ite (= (interpret-move-obstacle-0 start 1) end) 1  -1)))
+
+(define-fun get-move-obstacle-1 (( start Int ) ( end Int)) Int
+	(ite (= (interpret-move-obstacle-1 start 0) end) 0 
+	(ite (= (interpret-move-obstacle-1 start 1) end) 1 
+	(ite (= (interpret-move-obstacle-1 start 2) end) 2  -1))))
+
+(define-fun no-overlap-one-move-combination-2-2 ((p0 Int) (p1 Int) (p2 Int) (p3 Int)) Bool
+	(and (not (= p0 p2)) (and (not (= p0 p3)) (and (not (= p1 p2)) (and (not (= p1 p3)) true)))))
+
+(define-fun no-overlaps-0 (( currPoint Int ) ( move Int) (obstacleCurrPoint Int) (obstacleMove Int)) Bool
+	(= 1
+	(ite (= move 0) 
+		(ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
+		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0))
+	(ite (= move 1) 
+		(ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
+		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0))
+	(ite (= move 2) 
+		(ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
+		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0))
+	(ite (= move 3) 
+		(ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) -10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
+		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) -10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0))
+	(ite (= move 4) 
+		(ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint -1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
+		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint -1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0)) 0)))))))
+
+(define-fun no-overlaps-1 (( currPoint Int ) ( move Int) (obstacleCurrPoint Int) (obstacleMove Int)) Bool
+	(= 1
+	(ite (= move 0) 
+		(ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
+		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0)
+		(ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0)))
+	(ite (= move 1) 
+		(ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
+		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0)
+		(ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0)))
+	(ite (= move 2) 
+		(ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
+		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0)
+		(ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0)))
+	(ite (= move 3) 
+		(ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) -10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
+		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) -10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0)
+		(ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) -10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0)))
+	(ite (= move 4) 
+		(ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint -1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
+		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint -1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0)
+		(ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint -1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0))) 0)))))))
+
+(define-fun no-overlaps-one-step-helper ((currPoint Int) (move Int) (o0-t Int) (o0move Int) (o1-t Int) (o1move Int)) Bool
+	(and (no-overlaps-0 currPoint move o0-t o0move) (and (no-overlaps-1 currPoint move o1-t o1move) true)))
+
+(define-fun no-overlaps-one-step ((currPoint Int) (move Int)  (o0-0 Int) (o0-1 Int) (o1-0 Int) (o1-1 Int)) Bool
+	(no-overlaps-one-step-helper currPoint move o0-0 (get-move-obstacle-0 o0-0 o0-1) o1-0 (get-move-obstacle-1 o1-0 o1-1)))
+
+
+
+(declare-var o0-1 Int)
+(declare-var o0-2 Int)
+(declare-var o0-3 Int)
+(declare-var o1-1 Int)
+(declare-var o1-2 Int)
+(declare-var o1-3 Int)
+
+(synth-fun move ((currPoint Int) (o0 Int) (o1 Int)) Int
+	((Start Int (
+		MoveId
+		(ite StartBool Start Start)))
+    (MoveId Int (0
+		1
+		2
+		3
+		4
+  	))
+	(CondInt Int (
+		(get-y currPoint) ;y coord
+		(get-x currPoint) ;x coord
+		(get-y o0)
+		(get-x o0)
+		(get-y o1)
+		(get-x o1)
+		(+ CondInt CondInt)
+		(- CondInt CondInt)
+		-1
+		0
+		1
+		2
+		3
+		4
+		5
+		6
+		7
+		8
+		9
+				))
+	(StartBool Bool ((and StartBool StartBool)
+		(or  StartBool StartBool)
+		(not StartBool)
+		(<=  CondInt CondInt)
+		(=   CondInt CondInt)
+		(>=  CondInt CondInt))))) 
+ 
+ (constraint  (let ((pos0 Int 0)) (let ((mov0 Int (move pos0 99 98))) (let ((pos1 Int (interpret-move pos0 mov0))) (let ((mov1 Int (move pos1 o0-1 o1-1))) (let ((pos2 Int (interpret-move pos1 mov1))) (let ((mov2 Int (move pos2 o0-2 o1-2))) (let ((pos3 Int (interpret-move pos2 mov2)))
+ (or 
+	(and
+		(= pos3 30)
+		(and (no-overlaps-one-step pos0 mov0 99 o0-1 98 o1-1) (and (no-overlaps-one-step pos1 mov1 o0-1 o0-2 o1-1 o1-2) (and (no-overlaps-one-step pos2 mov2 o0-2 o0-3 o1-2 o1-3) true))))
+	(not (and (allowable-move-obstacle-0 99 o0-1) (and (allowable-move-obstacle-0 o0-1 o0-2) (and (allowable-move-obstacle-0 o0-2 o0-3) (and (allowable-move-obstacle-1 98 o1-1) (and (allowable-move-obstacle-1 o1-1 o1-2) (and (allowable-move-obstacle-1 o1-2 o1-3) true))))))))))))))))
+
+(check-synth)
diff --git a/test/regress/regress1/sygus/Makefile.am b/test/regress/regress1/sygus/Makefile.am
index ed8755236..17b8e8872 100644
--- a/test/regress/regress1/sygus/Makefile.am
+++ b/test/regress/regress1/sygus/Makefile.am
@@ -26,7 +26,8 @@ TESTS =	\
 	unbdd_inv_gen_ex7.sy \
 	icfp_easy_mt_ite.sy \
 	three.sy \
-	nia-max-square.sy
+	nia-max-square.sy \
+	MPwL_d1s3.sy
 
 EXTRA_DIST = $(TESTS)