1 files changed, 18 insertions, 2 deletions
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index d80a7cf82..25e5bbb5f 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -14,12 +14,13 @@
 
 #include "theory/quantifiers/quantifiers_attributes.h"
 
-#include "theory/quantifiers_engine.h"
 #include "options/quantifiers_options.h"
-#include "theory/quantifiers/sygus/ce_guided_instantiation.h"
+#include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/fun_def_engine.h"
 #include "theory/quantifiers/rewrite_engine.h"
+#include "theory/quantifiers/sygus/ce_guided_instantiation.h"
 #include "theory/quantifiers/term_util.h"
+#include "theory/quantifiers_engine.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -146,6 +147,21 @@ Node QuantAttributes::getFunDefBody( Node q ) {
       }else if( q[1][1]==h ){
         return q[1][0];
       }
+      else if (q[1][0].getType().isReal())
+      {
+        // solve for h in the equality
+        std::map<Node, Node> msum;
+        if (ArithMSum::getMonomialSum(q[1], msum))
+        {
+          Node veq;
+          int res = ArithMSum::isolate(h, msum, veq, EQUAL);
+          if (res != 0)
+          {
+            Assert(veq.getKind() == EQUAL);
+            return res == 1 ? veq[0] : veq[1];
+          }
+        }
+      }
     }else{
       Node atom = q[1].getKind()==NOT ? q[1][0] : q[1];
       bool pol = q[1].getKind()!=NOT;