Fix check for subtypes in sygus PBE (#3640)

diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index 0fa857c916aad65b063b3b279ef038b7a8686693..5468a1e6ac33d2ee22fe5d54781f372bc8ff53f3 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -420,7 +420,7 @@ Node SygusPbe::addSearchVal(TypeNode tn, Node e, Node bvr)
         d_sygus_unif[ee].clearExampleCache(e, bvr);
       }
     }
-    Assert(ret.getType() == bvr.getType());
+    Assert(ret.getType().isComparableTo(bvr.getType()));
     return ret;
   }
   return Node::null();

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index ed9ddda1befbb063e9c262a6db196447c7c90a9f..8212c21f10494ebcfdaf2b1eb2d18f4e54fde1a9 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1784,6 +1784,7 @@ set(regress_1_tests
   regress1/sygus/issue3514.smt2
   regress1/sygus/issue3507.smt2
   regress1/sygus/issue3580.sy
+  regress1/sygus/issue3634.smt2
   regress1/sygus/large-const-simp.sy
   regress1/sygus/let-bug-simp.sy
   regress1/sygus/list-head-x.sy

diff --git a/test/regress/regress1/sygus/issue3634.smt2 b/test/regress/regress1/sygus/issue3634.smt2
new file mode 100644 (file)
index 0000000..c7d5f91
--- /dev/null
+++ b/test/regress/regress1/sygus/issue3634.smt2
@@ -0,0 +1,7 @@
+; EXPECT: sat
+; COMMAND-LINE: --sygus-inference
+(set-logic ALL)
+(declare-fun a () Int)
+(declare-fun b () Real)
+(assert (= (/ 1 (to_real a)) b))
+(check-sat)