Update

cvc5 · Feb 1, 2024 · b51d495 · b51d495
1 parent 949f277
commit b51d495
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 14 deletions.
diff --git a/src/state.cpp b/src/state.cpp
@@ -484,18 +484,7 @@ Expr State::mkBuiltinType(Kind k)
 
 Expr State::mkAnnotatedType(const Expr& t, Attr ck, const Expr& cons)
 {
-  if (ck==Attr::BINDER)
-  {
-    // prepend to argument types the return type of the constructor
-    Expr c = cons;
-    const Expr& ct = d_tc.getType(c);
-    if (ct.getKind()!=Kind::FUNCTION_TYPE || ct[1].getKind()!=Kind::FUNCTION_TYPE)
-    {
-      return d_null;
-    }
-    return mkFunctionType({ct[1][1]}, t);
-  }
-  else if (ck!=Attr::RIGHT_ASSOC_NIL && ck!=Attr::LEFT_ASSOC_NIL)
+  if (ck!=Attr::RIGHT_ASSOC_NIL && ck!=Attr::LEFT_ASSOC_NIL)
   {
     return t;
   }

diff --git a/tests/binder-ex.smt3 b/tests/binder-ex.smt3
@@ -5,7 +5,7 @@
 (declare-sort Int 0)
 
 (declare-const P (-> Int Bool))
-(declare-const forall (-> Bool Bool) :binder @list.cons)
+(declare-const forall (-> @List Bool Bool) :binder @list.cons)
 
 (declare-rule id ((y Bool)) :premises (y) :conclusion y)
 

diff --git a/tests/binder-subterm-share.smt3 b/tests/binder-subterm-share.smt3
@@ -4,7 +4,7 @@
 
 (declare-sort Int 0)
 (declare-const P (-> Int Bool))
-(declare-const forall (-> Bool Bool) :binder @list.cons)
+(declare-const forall (-> @List Bool Bool) :binder @list.cons)
 (declare-rule id ((y Bool)) :premises (y) :conclusion y)
 
 (declare-var x Int)