From 84a4d9850b6aa7eed17c02a3d6b6b0332e328c59 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 12 Apr 2020 18:00:43 -0700
Subject: [PATCH] fix #3936

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_dense_diff_logic_def.h | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h
index 6b86e718c..bc0e9342c 100644
--- a/src/smt/theory_dense_diff_logic_def.h
+++ b/src/smt/theory_dense_diff_logic_def.h
@@ -392,6 +392,8 @@ namespace smt {
 
     template<typename Ext>
     final_check_status theory_dense_diff_logic<Ext>::final_check_eh() {
+        //fix_zero();
+        //compute_epsilon();
         init_model();
         if (assume_eqs(m_var_value_table))
             return FC_CONTINUE;
@@ -768,7 +770,7 @@ namespace smt {
     */
     template<typename Ext>
     void theory_dense_diff_logic<Ext>::compute_epsilon() {
-        m_epsilon = rational(1);
+        m_epsilon = rational(1, 2);
         typename edges::const_iterator it  = m_edges.begin();
         typename edges::const_iterator end = m_edges.end();
         // first edge is null