From 62f8cc1289f925adc416bef90eab3ef3657dcf55 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 31 Aug 2017 07:33:38 -0700
Subject: [PATCH] fix ordering for value propagation to ensure values are
 preferred

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/asserted_formulas.cpp | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp
index 626588ab3..6ecf26bd8 100644
--- a/src/smt/asserted_formulas.cpp
+++ b/src/smt/asserted_formulas.cpp
@@ -514,9 +514,15 @@ bool asserted_formulas::is_gt(expr* lhs, expr* rhs) {
     if (lhs == rhs) {
         return false;
     }
-    if (m.is_value(rhs)) {
+    // values are always less in ordering than non-values.
+    bool v1 = m.is_value(lhs);
+    bool v2 = m.is_value(rhs);
+    if (!v1 && v2) {
         return true;
     }
+    if (v1 && !v2) {
+        return false;
+    }
     SASSERT(is_ground(lhs) && is_ground(rhs));
     if (depth(lhs) > depth(rhs)) {
         return true;