Repository: dreal/dreal4 (language: python)

Issue:
Unsoundness for large formulas with integer variables in the C++ interface.
In some cases when using the C++ interface, dReal will return unsat for formulas over integer variables which are actually satisfiable. For example, running [this code](https://gist.github.com/gavlegoat/98c10bb069e7becc21d20a25fe02f1e0) as written yields unsat. However if I copy this formula to an SMT2 file and use the dReal executable, dReal successfully finds a satisfying assignment. Uncommenting the first line of the formula in that gist forces dReal to use the correct assignment, and in that case the C++ code does indeed return sat.

I have only seen this happen with relatively large formulas like the attached one, on smaller formulas there doesn't seem to be any issue.

This behavior was tested with dReal version 4.21.06.1, installed with the .deb package on Mint 19.3 (based on Ubuntu 18.04). I had also seen this when using dReal version 4.20.07.1.


Discussion / hints:
Thanks for the report, @gavlegoat . I'll investigate this and get back to you.
I have been digging into this some more and I think I was wrong and this is not a C++ issue. Instead there seems to be some sensitivity to the representation of the formula. Specifically, if you look at [this gist](https://gist.github.com/gavlegoat/510f9d800a4540ed85faa08cbd4a1459), there are two different versions of the same formula (this is also the same formula from the initial post). The only difference between these two is that in `minus.smt2` there are several expressions of the form `(> (+ (- (+ t1 (* c1 t2)) (* c2 t3)) (* c3 t4)) 0)` where `c1`, `c2`, and `c3` are constants and `t1` through `t4` are variables. In `plus.smt2` those expressions are replaced by `(> (+ (+ t1 (* c1 t2)) (* -c2 t3) (* c3 t4)) 0)`. These should be equivalent but `plus.smt2` returns unsat while `minus.smt2` returns sat.

In order to try to rule out delta-completeness issues I also tried running these with varying precision. `plus.smt2` is unsat even for very large delta (as high as 1) and `minus.smt2` is sat even for delta as small as 1e-9.
@gavlegoat , could you test it using the current HEAD (`b1d1341`)? When I check the two SMT2 files (plus and minus), both of the return `sat` (precision = 0.001).
FWIW, I fixed a bug about two weeks ago, but have not released a new version yet. I'll prepare binaries today.

08d2d6c fix(contractor/contractor_integer): Fix a bug Soonho Kong, 12 days ago

I'm getting the same result running in HEAD (plus is unsat and minus is sat). I also tried rerunning install_prereqs to make sure I have the most recent versions of all dependencies, but that didn't fix the problem either. What OS are you using? Maybe there is an issue in the Ubuntu 18.04 dependencies.
Thanks for the check. I was using macOS. I'll test it on an Ubuntu machine.
I can reproduce it on my Ubuntu box. I'll let you know when I find my information about this bug.
In case it is helpful, a colleague was able to reproduce this issue using MacOS 10.15.7, using the version of dReal from HEAD.
@gavlegoat , thanks for the check. I was also able to reproduce it on my mac (maybe there was a glitch last time I tried). I'm still debugging the code but will get back to you when I have more info.

Fix patch:
diff --git a/dreal/contractor/contractor_status.cc b/dreal/contractor/contractor_status.cc
index 169de2cc..b1074af3 100644
--- a/dreal/contractor/contractor_status.cc
+++ b/dreal/contractor/contractor_status.cc
@@ -99,9 +99,6 @@ set<Formula> GenerateExplanation(const Variables& unsat_witness,
   static ContractorStatusStat stat(DREAL_LOG_INFO_ENABLED);
   stat.increase_num_explanation_generation();
   TimerGuard timer_guard(&stat.timer_explanation_generation_, stat.enabled());
-  if (unsat_witness.empty()) {
-    return set<Formula>();
-  }
 
   // Explanation:
   // = lfp. λE. E ∪ {fᵢ | fᵢ ∈ Used Constraints ∧ vars(fᵢ) ∩ unsat_witness ≠ ∅}
@@ -112,10 +109,24 @@ set<Formula> GenerateExplanation(const Variables& unsat_witness,
   // Set up the initial explanation based on variables.
   set<Formula> explanation;
   for (const Formula& f_i : used_constraints) {
+    if (f_i.GetFreeVariables().empty()) {
+      // It is possible that the constraint has no free variable but
+      // we can't decide its truth value. For example, in SMT2, (0.01
+      // < 1.0) will be translated into a formula with intervals and
+      // we don't do constant-folding over intervals yet, so it
+      // remains as it is.
+      explanation.insert(f_i);
+      continue;
+    }
     if (HaveIntersection(unsat_witness, f_i.GetFreeVariables())) {
       explanation.insert(f_i);
     }
   }
+
+  if (unsat_witness.empty()) {
+    return explanation;
+  }
+
   bool keep_going = true;
   while (keep_going) {
     keep_going = false;
diff --git a/dreal/solver/context_impl.cc b/dreal/solver/context_impl.cc
index 1d93757f..7a8138e9 100644
--- a/dreal/solver/context_impl.cc
+++ b/dreal/solver/context_impl.cc
@@ -170,6 +170,14 @@ optional<Box> Context::Impl::CheckSatCore(const ScopedVector<Formula>& stack,
               "size = {}",
               explanation.size(), stack.get_vector().size());
           sat_solver->AddLearnedClause(explanation);
+          if (DREAL_LOG_TRACE_ENABLED) {
+            for (const auto& f_i : stack.get_vector()) {
+              DREAL_LOG_TRACE("ContextImpl::CheckSatCore: Stack {}", f_i);
+            }
+            for (const auto& f_i : explanation) {
+              DREAL_LOG_TRACE("ContextImpl::CheckSatCore: Explanation {}", f_i);
+            }
+          }
         }
       } else {
         return box;
diff --git a/dreal/solver/sat_solver.cc b/dreal/solver/sat_solver.cc
index 938bee23..0d33d8a3 100644
--- a/dreal/solver/sat_solver.cc
+++ b/dreal/solver/sat_solver.cc
@@ -111,7 +111,7 @@ optional<SatSolver::Model> SatSolver::CheckSat() {
   // Call SAT solver.
   TimerGuard check_sat_timer_guard(&stat.timer_check_sat_,
                                    DREAL_LOG_INFO_ENABLED);
-  const int ret{picosat_sat(sat_, -1)};
+  const int ret{picosat_sat(sat_, -1 /* decision_limit == no limit */)};
   check_sat_timer_guard.pause();
 
   Model model;
@@ -135,19 +135,19 @@ optional<SatSolver::Model> SatSolver::CheckSat() {
       const auto it = var_to_formula_map.find(var);
       if (it != var_to_formula_map.end()) {
         DREAL_LOG_TRACE("SatSolver::CheckSat: Add theory literal {}{} to Model",
-                        model_i ? "" : "¬", var);
+                        model_i == 1 ? "" : "¬", var);
         auto& theory_model = model.second;
         theory_model.emplace_back(var, model_i == 1);
       } else if (tseitin_variables_.count(var.get_id()) == 0) {
         DREAL_LOG_TRACE(
             "SatSolver::CheckSat: Add Boolean literal {}{} to Model ",
-            model_i ? "" : "¬", var);
+            model_i == 1 ? "" : "¬", var);
         auto& boolean_model = model.first;
         boolean_model.emplace_back(var, model_i == 1);
       } else {
         DREAL_LOG_TRACE(
             "SatSolver::CheckSat: Skip {}{} which is a temporary variable.",
-            model_i ? "" : "¬", var);
+            model_i == 1 ? "" : "¬", var);
       }
     }
     DREAL_LOG_DEBUG("SatSolver::CheckSat() Found a model.");
diff --git a/dreal/solver/theory_solver.cc b/dreal/solver/theory_solver.cc
index 080983c0..77c32e07 100644
--- a/dreal/solver/theory_solver.cc
+++ b/dreal/solver/theory_solver.cc
@@ -109,6 +109,9 @@ optional<Contractor> TheorySolver::BuildContractor(
       case FilterAssertionResult::FilteredWithChange:
         contractor_status->AddUsedConstraint(f);
         if (box.empty()) {
+          for (const auto& v : f.GetFreeVariables()) {
+            contractor_status->AddUnsatWitness(v);
+          }
           return {};
         }
         continue;


Test patch:
diff --git a/dreal/test/smt2/BUILD.bazel b/dreal/test/smt2/BUILD.bazel
index 5ffd0383..1a5c8189 100644
--- a/dreal/test/smt2/BUILD.bazel
+++ b/dreal/test/smt2/BUILD.bazel
@@ -1180,6 +1180,16 @@ smt2_test(
     size = "small",
 )
 
+smt2_test(
+    name = "github_issue_250_plus",
+    size = "small",
+)
+
+smt2_test(
+    name = "github_issue_250_minus",
+    size = "small",
+)
+
 smt2_test(
     name = "xor_01",
     size = "small",
diff --git a/dreal/test/smt2/github_issue_184.smt2.expected b/dreal/test/smt2/github_issue_184.smt2.expected
index 3f65111b..a0270033 100644
--- a/dreal/test/smt2/github_issue_184.smt2.expected
+++ b/dreal/test/smt2/github_issue_184.smt2.expected
@@ -1,1 +1,1 @@
-unsat
+delta-sat with delta = 0.001
diff --git a/dreal/test/smt2/github_issue_250_minus.smt2 b/dreal/test/smt2/github_issue_250_minus.smt2
new file mode 100644
index 00000000..61f77d95
--- /dev/null
+++ b/dreal/test/smt2/github_issue_250_minus.smt2
@@ -0,0 +1,83 @@
+(declare-fun t1 () Int)
+(declare-fun t2 () Int)
+(declare-fun t3 () Int)
+(declare-fun t4 () Int)
+(declare-fun t5 () Int)
+(declare-fun t6 () Int)
+
+(assert
+(and
+(> (+ (- (+ t3 (* 1.000000 t4)) (* 4 t5)) (* 16.000000 t6)) 0)
+(> (+ (- (+ t3 (* 1.000000 t4)) (* 4.000000 t5)) (* 16.000000 t6)) 0)
+(> (+ (- (+ t3 (* 1.000000 t4)) (* 2.000000 t5)) (* 4.000000 t6)) 0)
+(> (+ (- (+ t3 (* 1.000000 t4)) (* 1.618034 t5)) (* 2.618034 t6)) 0)
+(> (+ (- (+ t3 (* 1.000000 t4)) (* 2.414214 t5)) (* 5.828427 t6)) 0)
+(> (+ (+ t3 (* 1.005066 t4)) (* 3.005631 t5) (* 8.988285 t6)) 0)
+(> (+ (- (+ t3 (* 1.044753 t4)) (* 0.537527 t5)) (* 0.276559 t6)) 0)
+(> (+ (- (+ t3 (* 1.198125 t4)) (* 0.761081 t5)) (* 0.483459 t6)) 0)
+(> (+ (- (+ t3 (* 1.217888 t4)) (* 3.859908 t5)) (* 12.233388 t6)) 0)
+(> (+ (+ t3 (* 1.218265 t4)) (* 0.140590 t5) (* 0.016224 t6)) 0)
+(> (+ (- (+ t3 (* 1.266452 t4)) (* 0.885198 t5)) (* 0.618717 t6)) 0)
+(> (+ (- (+ t3 (* 1.624399 t4)) (* 3.784773 t5)) (* 8.818344 t6)) 0)
+(> (+ (- (+ t3 (* 2.214483 t4)) (* 5.749637 t5)) (* 14.928240 t6)) 0)
+(> (+ (+ t3 (* 2.626278 t4)) (* 4.138619 t5) (* 6.521840 t6)) 0)
+(> (+ (+ t3 (* 2.727082 t4)) (* -6.212318 t5) (* 14.151717 t6)) 0)
+(> (+ t3 (* 4.515625 t4)) 0)
+(> (+ (+ (+ t3 (* 4.515625 t4)) (* 6.375000 t5)) (* 9 t6)) 0)
+(> (+ (- (+ t3 (* 10.562500 t4)) (* 10.562500 t5)) (* 10.562500 t6)) 0)
+(> (+ (+ (+ t3 (* 15.627197 t4)) (* 8.274397 t5)) (* 4.381186 t6)) 0)
+(>= t1 -16)
+(>= t2 -16)
+(>= t3 -16)
+(>= t4 -16)
+(>= t5 -16)
+(>= t6 -16)
+(<= t1 16)
+(<= t2 16)
+(<= t3 16)
+(<= t4 16)
+(<= t5 16)
+(<= t6 16)
+(or (> (+ (+ (+ t3 (* 0.391934 t4)) (* 0.550236 t5)) (* 0.772476 t6)) 0) (<= (+ (- (+ t3 (* 0.509706 t4)) (* 0.713937 (* t5 (+ -0.878906 (* 0.100000 (+ (- (- (* 0.626047 t1)) (* 0.878906 t2)) (sin -0.626047))))))) (* t6 (pow (+ -0.878906 (* 0.100000 (+ (- (- (* 0.626047 t1)) (* 0.878906 t2)) (sin -0.626047)))) 2))) 0))
+(or (> (+ (+ (+ t3 (* 0.404340 t4)) (* 0.596445 t5)) (* 0.879822 t6)) 0) (<= (+ (- (+ t3 (* 0.532427 t4)) (* 0.729676 (* t5 (+ -0.937988 (* 0.100000 (+ (- (- (* 0.635877 t1)) (* 0.937988 t2)) (sin -0.635877))))))) (* t6 (pow (+ -0.937988 (* 0.100000 (+ (- (- (* 0.635877 t1)) (* 0.937988 t2)) (sin -0.635877)))) 2))) 0))
+(or (> (+ (- (+ t3 t4) (* 0.000000 t5)) (* 0.000000 t6)) 0) (<= (+ (+ (+ t3 t4) (* t5 (+ -0.000000 (* 0.100000 (+ (- t1 (* 0.000000 t2)) (sin 1)))))) (* t6 (pow (+ -0.000000 (* 0.100000 (+ (- t1 (* 0.000000 t2)) (sin 1)))) 2))) 0))
+(or (> (+ (- (+ t3 t4) (* 0.000000 t5)) (* 0.000000 t6)) 0) (<= (+ (+ (+ t3 t4) (* t5 (+ -0.000000 (* 0.100000 (+ (- t1 (* 0.000000 t2)) (sin 1)))))) (* t6 (pow (+ -0.000000 (* 0.100000 (+ (- t1 (* 0.000000 t2)) (sin 1)))) 2))) 0))
+(or (> (+ (- (+ t3 t4) (* 0.000000 t5)) (* 0.000000 t6)) 0) (<= (+ (+ (+ t3 t4) (* t5 (+ -0.000000 (* 0.100000 (+ (- t1 (* 0.000000 t2)) (sin 1)))))) (* t6 (pow (+ -0.000000 (* 0.100000 (+ (- t1 (* 0.000000 t2)) (sin 1)))) 2))) 0))
+(or (> (+ (- (+ t3 t4) (* 0.000000 t5)) (* 0.000000 t6)) 0) (<= (+ (+ (+ t3 t4) (* t5 (+ -0.000000 (* 0.100000 (+ (- t1 (* 0.000000 t2)) (sin 1)))))) (* t6 (pow (+ -0.000000 (* 0.100000 (+ (- t1 (* 0.000000 t2)) (sin 1)))) 2))) 0))
+(or (> (+ (+ (+ t3 t4) (* 0.000000 t5)) (* 0.000000 t6)) 0) (<= (+ (- (+ t3 (* 1.000000 t4)) (* 1.000000 (* t5 (+ -0.000000 (* 0.100000 (+ (- (- t1) (* 0.000000 t2)) (sin -1))))))) (* t6 (pow (+ -0.000000 (* 0.100000 (+ (- (- t1) (* 0.000000 t2)) (sin -1)))) 2))) 0))
+(or (> (+ (- (+ t3 (* 1.000000 t4)) (* 4 t5)) (* 16.000000 t6)) 0) (<= (+ (+ (+ t3 (* 0.360000 t4)) (* 0.600000 (* t5 (+ -4.000000 (* 0.100000 (+ (- (* 1.000000 t1) (* 4.000000 t2)) (sin 1.000000))))))) (* t6 (pow (+ -4.000000 (* 0.100000 (+ (- (* 1.000000 t1) (* 4.000000 t2)) (sin 1.000000)))) 2))) 0))
+(or (> (+ (- (+ t3 (* 1.000000 t4)) (* 4.000000 t5)) (* 16.000000 t6)) 0) (<= (+ (+ (+ t3 (* 0.360000 t4)) (* 0.600000 (* t5 (+ -4.000000 (* 0.100000 (+ (- (* 1.000000 t1) (* 4.000000 t2)) (sin 1.000000))))))) (* t6 (pow (+ -4.000000 (* 0.100000 (+ (- (* 1.000000 t1) (* 4.000000 t2)) (sin 1.000000)))) 2))) 0))
+(or (> (+ (- (+ t3 (* 1.000000 t4)) (* 2.000000 t5)) (* 4.000000 t6)) 0) (<= (+ (+ (+ t3 (* 0.640000 t4)) (* 0.800000 (* t5 (+ -2.000000 (* 0.100000 (+ (- (* 1.000000 t1) (* 2.000000 t2)) (sin 1.000000))))))) (* t6 (pow (+ -2.000000 (* 0.100000 (+ (- (* 1.000000 t1) (* 2.000000 t2)) (sin 1.000000)))) 2))) 0))
+(or (> (+ (- (+ t3 (* 1.000000 t4)) (* 1.618034 t5)) (* 2.618034 t6)) 0) (<= (+ (+ (+ t3 (* 0.702574 t4)) (* 0.838197 (* t5 (+ -1.618034 (* 0.100000 (+ (- (* 1.000000 t1) (* 1.618034 t2)) (sin 1.000000))))))) (* t6 (pow (+ -1.618034 (* 0.100000 (+ (- (* 1.000000 t1) (* 1.618034 t2)) (sin 1.000000)))) 2))) 0))
+(or (> (+ (- (+ t3 (* 1.000000 t4)) (* 2.414214 t5)) (* 5.828427 t6)) 0) (<= (+ (+ (+ t3 (* 0.575442 t4)) (* 0.758579 (* t5 (+ -2.414214 (* 0.100000 (+ (- (* 1.000000 t1) (* 2.414214 t2)) (sin 1.000000))))))) (* t6 (pow (+ -2.414214 (* 0.100000 (+ (- (* 1.000000 t1) (* 2.414214 t2)) (sin 1.000000)))) 2))) 0))
+(or (> (+ (+ (+ t3 (* 1.005066 t4)) (* 3.005631 t5)) (* 8.988285 t6)) 0) (<= (+ (- (+ t3 (* 1.696075 t4)) (* 1.302334 (* t5 (+ -2.998047 (* 0.100000 (+ (- (- (* 1.002530 t1)) (* 2.998047 t2)) (sin -1.002530))))))) (* t6 (pow (+ -2.998047 (* 0.100000 (+ (- (- (* 1.002530 t1)) (* 2.998047 t2)) (sin -1.002530)))) 2))) 0))
+(or (> (+ (- (+ t3 (* 1.044753 t4)) (* 0.537527 t5)) (* 0.276559 t6)) 0) (<= (+ (+ (+ t3 (* 0.940013 t4)) (* 0.969543 (* t5 (+ -0.525888 (* 0.100000 (+ (- (* 1.022131 t1) (* 0.525888 t2)) (sin 1.022131))))))) (* t6 (pow (+ -0.525888 (* 0.100000 (+ (- (* 1.022131 t1) (* 0.525888 t2)) (sin 1.022131)))) 2))) 0))
+(or (> (+ (- (+ t3 (* 1.198125 t4)) (* 0.761081 t5)) (* 0.483459 t6)) 0) (<= (+ (+ (+ t3 (* 1.050743 t4)) (* 1.025058 (* t5 (+ -0.695313 (* 0.100000 (+ (- (* 1.094589 t1) (* 0.695313 t2)) (sin 1.094589))))))) (* t6 (pow (+ -0.695313 (* 0.100000 (+ (- (* 1.094589 t1) (* 0.695313 t2)) (sin 1.094589)))) 2))) 0))
+(or (> (+ (- (+ t3 (* 1.217888 t4)) (* 3.859908 t5)) (* 12.233388 t6)) 0) (<= (+ (+ (+ t3 (* 0.568240 t4)) (* 0.753817 (* t5 (+ -3.497626 (* 0.100000 (+ (- (* 1.103579 t1) (* 3.497626 t2)) (sin 1.103579))))))) (* t6 (pow (+ -3.497626 (* 0.100000 (+ (- (* 1.103579 t1) (* 3.497626 t2)) (sin 1.103579)))) 2))) 0))
+(or (> (+ (+ (+ t3 (* 1.218265 t4)) (* 0.140590 t5)) (* 0.016224 t6)) 0) (<= (+ (- (+ t3 (* 1.246545 t4)) (* 1.116488 (* t5 (+ -0.127374 (* 0.100000 (+ (- (- (* 1.103750 t1)) (* 0.127374 t2)) (sin -1.103750))))))) (* t6 (pow (+ -0.127374 (* 0.100000 (+ (- (- (* 1.103750 t1)) (* 0.127374 t2)) (sin -1.103750)))) 2))) 0))
+(or (> (+ (- (+ t3 (* 1.266452 t4)) (* 0.885198 t5)) (* 0.618717 t6)) 0) (<= (+ (+ (+ t3 (* 1.095600 t4)) (* 1.046709 (* t5 (+ -0.786585 (* 0.100000 (+ (- (* 1.125368 t1) (* 0.786585 t2)) (sin 1.125368))))))) (* t6 (pow (+ -0.786585 (* 0.100000 (+ (- (* 1.125368 t1) (* 0.786585 t2)) (sin 1.125368)))) 2))) 0))
+(or (> (+ (- (+ t3 (* 1.624399 t4)) (* 3.784773 t5)) (* 8.818344 t6)) 0) (<= (+ (+ (+ t3 (* 0.955628 t4)) (* 0.977562 (* t5 (+ -2.969570 (* 0.100000 (+ (- (* 1.274519 t1) (* 2.969570 t2)) (sin 1.274519))))))) (* t6 (pow (+ -2.969570 (* 0.100000 (+ (- (* 1.274519 t1) (* 2.969570 t2)) (sin 1.274519)))) 2))) 0))
+(or (> (+ (- (+ t3 (* 2.214483 t4)) (* 5.749637 t5)) (* 14.928240 t6)) 0) (<= (+ (+ (+ t3 (* 1.213838 t4)) (* 1.101743 (* t5 (+ -3.863708 (* 0.100000 (+ (- (* 1.488114 t1) (* 3.863708 t2)) (sin 1.488114))))))) (* t6 (pow (+ -3.863708 (* 0.100000 (+ (- (* 1.488114 t1) (* 3.863708 t2)) (sin 1.488114)))) 2))) 0))
+(or (> (+ (+ (+ t3 (* 2.626278 t4)) (* 4.138619 t5)) (* 6.521840 t6)) 0) (<= (+ (- (+ t3 (* 3.519221 t4)) (* 1.875959 (* t5 (+ -2.553789 (* 0.100000 (+ (- (- (* 1.620580 t1)) (* 2.553789 t2)) (sin -1.620580))))))) (* t6 (pow (+ -2.553789 (* 0.100000 (+ (- (- (* 1.620580 t1)) (* 2.553789 t2)) (sin -1.620580)))) 2))) 0))
+(or (> (+ (- (+ t3 (* 2.727082 t4)) (* 6.212318 t5)) (* 14.151717 t6)) 0) (<= (+ (+ (+ t3 (* 1.626135 t4)) (* 1.275200 (* t5 (+ -3.761877 (* 0.100000 (+ (- (* 1.651388 t1) (* 3.761877 t2)) (sin 1.651388))))))) (* t6 (pow (+ -3.761877 (* 0.100000 (+ (- (* 1.651388 t1) (* 3.761877 t2)) (sin 1.651388)))) 2))) 0))
+(or (> (+ t3 (* 4.515625 t4)) 0) (<= (+ (- (+ t3 (* 4.515625 t4)) (* 0.212500 (* t5 (+ (- (* 2.125000 t1)) (sin -2.125000))))) (* 0.010000 (* t6 (pow (+ (- (* 2.125000 t1)) (sin -2.125000)) 2)))) 0))
+(or (> (+ (+ (+ t3 (* 4.515625 t4)) (* 6.375000 t5)) (* 9 t6)) 0) (<= (+ (- (+ t3 (* 5.880625 t4)) (* 2.425000 (* t5 (+ -3 (* 0.100000 (+ (- (- (* 2.125000 t1)) (* 3 t2)) (sin -2.125000))))))) (* t6 (pow (+ -3 (* 0.100000 (+ (- (- (* 2.125000 t1)) (* 3 t2)) (sin -2.125000)))) 2))) 0))
+(or (> (+ (- (+ t3 (* 10.562500 t4)) (* 10.562500 t5)) (* 10.562500 t6)) 0) (<= (+ (+ (+ t3 (* 8.555625 t4)) (* 2.925000 (* t5 (+ -3.250000 (* 0.100000 (+ (- (* 3.250000 t1) (* 3.250000 t2)) (sin 3.250000))))))) (* t6 (pow (+ -3.250000 (* 0.100000 (+ (- (* 3.250000 t1) (* 3.250000 t2)) (sin 3.250000)))) 2))) 0))
+(or (> (+ (+ (+ t3 (* 15.627197 t4)) (* 8.274397 t5)) (* 4.381186 t6)) 0) (<= (+ (- (+ t3 (* 17.325889 t4)) (* 4.162438 (* t5 (+ -2.093128 (* 0.100000 (+ (- (- (* 3.953125 t1)) (* 2.093128 t2)) (sin -3.953125))))))) (* t6 (pow (+ -2.093128 (* 0.100000 (+ (- (- (* 3.953125 t1)) (* 2.093128 t2)) (sin -3.953125)))) 2))) 0))
+(or (> (+ t3 (* 2.250000 t6)) 0) (<= (+ (- (+ t3 (* 0.022500 t4)) (* 0.150000 (* t5 (+ -1.500000 (* 0.100000 (+ (- (* 1.500000 t2)) (sin 0))))))) (* t6 (pow (+ -1.500000 (* 0.100000 (+ (- (* 1.500000 t2)) (sin 0)))) 2))) 0))
+(or (>= t1 0.200000) (>= t2 -0.800000) (>= t3 -1.800000) (>= t4 2.200000) (>= t5 -0.800000) (>= t6 1.200000) (<= t1 -0.200000) (<= t2 -1.200000) (<= t3 -2.200000) (<= t4 1.800000) (<= t5 -1.200000) (<= t6 0.800000))
+(or (>= t1 0.200000) (>= t2 0.200000) (>= t3 -2.800000) (>= t4 3.200000) (>= t5 -3.800000) (>= t6 -0.800000) (<= t1 -0.200000) (<= t2 -0.200000) (<= t3 -3.200000) (<= t4 2.800000) (<= t5 -4.200000) (<= t6 -1.200000))
+(or (>= t1 0.200000) (>= t2 0.200000) (>= t3 -0.800000) (>= t4 1.200000) (>= t5 -0.800000) (>= t6 0.200000) (<= t1 -0.200000) (<= t2 -0.200000) (<= t3 -1.200000) (<= t4 0.800000) (<= t5 -1.200000) (<= t6 -0.200000))
+(or (>= t1 0.200000) (>= t2 0.200000) (>= t3 -0.800000) (>= t4 1.200000) (>= t5 -0.800000) (>= t6 1.200000) (<= t1 -0.200000) (<= t2 -0.200000) (<= t3 -1.200000) (<= t4 0.800000) (<= t5 -1.200000) (<= t6 0.800000))
+(or (>= t1 0.200000) (>= t2 0.200000) (>= t3 1.200000) (>= t4 1.200000) (>= t5 -0.800000) (>= t6 -0.800000) (<= t1 -0.200000) (<= t2 -0.200000) (<= t3 0.800000) (<= t4 0.800000) (<= t5 -1.200000) (<= t6 -1.200000))
+(or (>= t1 0.200000) (>= t2 1.200000) (>= t3 -1.800000) (>= t4 2.200000) (>= t5 -0.800000) (>= t6 0.200000) (<= t1 -0.200000) (<= t2 0.800000) (<= t3 -2.200000) (<= t4 1.800000) (<= t5 -1.200000) (<= t6 -0.200000))
+(or (>= t1 0.200000) (>= t2 1.200000) (>= t3 -0.800000) (>= t4 1.200000) (>= t5 -0.800000) (>= t6 1.200000) (<= t1 -0.200000) (<= t2 0.800000) (<= t3 -1.200000) (<= t4 0.800000) (<= t5 -1.200000) (<= t6 0.800000))
+(or (>= t1 1.200000) (>= t2 -1.800000) (>= t3 -0.800000) (>= t4 1.200000) (>= t5 -0.800000) (>= t6 0.200000) (<= t1 0.800000) (<= t2 -2.200000) (<= t3 -1.200000) (<= t4 0.800000) (<= t5 -1.200000) (<= t6 -0.200000))
+(or (>= t1 1.200000) (>= t2 -0.800000) (>= t3 -1.800000) (>= t4 2.200000) (>= t5 -0.800000) (>= t6 0.200000) (<= t1 0.800000) (<= t2 -1.200000) (<= t3 -2.200000) (<= t4 1.800000) (<= t5 -1.200000) (<= t6 -0.200000))
+(or (>= t1 2.200000) (>= t2 1.200000) (>= t3 -1.800000) (>= t4 2.200000) (>= t5 -0.800000) (>= t6 0.200000) (<= t1 1.800000) (<= t2 0.800000) (<= t3 -2.200000) (<= t4 1.800000) (<= t5 -1.200000) (<= t6 -0.200000))
+(or (>= t1 4.200000) (>= t2 0.200000) (>= t3 -1.800000) (>= t4 4.200000) (>= t5 -3.800000) (>= t6 -1.800000) (<= t1 3.800000) (<= t2 -0.200000) (<= t3 -2.200000) (<= t4 3.800000) (<= t5 -4.200000) (<= t6 -2.200000))
+(or (>= t1 4.200000) (>= t2 1.200000) (>= t3 -2.800000) (>= t4 3.200000) (>= t5 -0.800000) (>= t6 2.200000) (<= t1 3.800000) (<= t2 0.800000) (<= t3 -3.200000) (<= t4 2.800000) (<= t5 -1.200000) (<= t6 1.800000))
+(or (>= t1 4.200000) (>= t2 1.200000) (>= t3 -1.800000) (>= t4 2.200000) (>= t5 -2.800000) (>= t6 2.200000) (<= t1 3.800000) (<= t2 0.800000) (<= t3 -2.200000) (<= t4 1.800000) (<= t5 -3.200000) (<= t6 1.800000))
+(or (>= t1 15.200000) (>= t2 -11.800000) (>= t3 -1.800000) (>= t4 14.200000) (>= t5 -4.800000) (>= t6 -1.800000) (<= t1 14.800000) (<= t2 -12.200000) (<= t3 -2.200000) (<= t4 13.800000) (<= t5 -5.200000) (<= t6 -2.200000))))
+
+(check-sat)
diff --git a/dreal/test/smt2/github_issue_250_minus.smt2.expected b/dreal/test/smt2/github_issue_250_minus.smt2.expected
new file mode 100644
index 00000000..a0270033
--- /dev/null
+++ b/dreal/test/smt2/github_issue_250_minus.smt2.expected
@@ -0,0 +1,1 @@
+delta-sat with delta = 0.001
diff --git a/dreal/test/smt2/github_issue_250_plus.smt2 b/dreal/test/smt2/github_issue_250_plus.smt2
new file mode 100644
index 00000000..1fafe462
--- /dev/null
+++ b/dreal/test/smt2/github_issue_250_plus.smt2
@@ -0,0 +1,102 @@
+(declare-fun t1 () Int [-16,16])
+(declare-fun t2 () Int [-16,16])
+(declare-fun t3 () Int [-16,16])
+(declare-fun t4 () Int [-16,16])
+(declare-fun t5 () Int [-16,16])
+(declare-fun t6 () Int [-16,16])
+
+;; (declare-fun t1 () Int [0,0])
+;; (declare-fun t2 () Int [-5,-5])
+;; (declare-fun t3 () Int [-2,-2])
+;; (declare-fun t4 () Int [2,2])
+;; (declare-fun t5 () Int [-1,-1])
+;; (declare-fun t6 () Int [1,1])
+
+;; t1 : [0, 0]
+;; t2 : [-5, -5]
+;; t3 : [-2, -2]
+;; t4 : [2, 2]
+;; t5 : [-1, -1]
+;; t6 : [1, 1]
+
+
+(assert
+(and
+(> (+ (+ t3 (* 1.000000 t4)) (* -4 t5) (* 16.000000 t6)) 0)
+(> (+ (+ t3 (* 1.000000 t4)) (* -4.000000 t5) (* 16.000000 t6)) 0)
+(> (+ (+ t3 (* 1.000000 t4)) (* -2.000000 t5) (* 4.000000 t6)) 0)
+(> (+ (+ t3 (* 1.000000 t4)) (* -1.618034 t5) (* 2.618034 t6)) 0)
+(> (+ (+ t3 (* 1.000000 t4)) (* -2.414214 t5) (* 5.828427 t6)) 0)
+(> (+ (+ t3 (* 1.005066 t4)) (* 3.005631 t5) (* 8.988285 t6)) 0)
+(> (+ (+ t3 (* 1.044753 t4)) (* -0.537527 t5) (* 0.276559 t6)) 0)
+(> (+ (+ t3 (* 1.198125 t4)) (* -0.761081 t5) (* 0.483459 t6)) 0)
+(> (+ (+ t3 (* 1.217888 t4)) (* -3.859908 t5) (* 12.233388 t6)) 0)
+(> (+ (+ t3 (* 1.218265 t4)) (* 0.140590 t5) (* 0.016224 t6)) 0)
+(> (+ (+ t3 (* 1.266452 t4)) (* -0.885198 t5) (* 0.618717 t6)) 0)
+(> (+ (+ t3 (* 1.624399 t4)) (* -3.784773 t5) (* 8.818344 t6)) 0)
+(> (+ (+ t3 (* 2.214483 t4)) (* -5.749637 t5) (* 14.928240 t6)) 0)
+(> (+ (+ t3 (* 2.626278 t4)) (* 4.138619 t5) (* 6.521840 t6)) 0)
+(> (+ (+ t3 (* 2.727082 t4)) (* -6.212318 t5) (* 14.151717 t6)) 0)
+(> (+ t3 (* 4.515625 t4)) 0)
+(> (+ (+ (+ t3 (* 4.515625 t4)) (* 6.375000 t5)) (* 9 t6)) 0)
+(> (+ (- (+ t3 (* 10.562500 t4)) (* 10.562500 t5)) (* 10.562500 t6)) 0)
+(> (+ (+ (+ t3 (* 15.627197 t4)) (* 8.274397 t5)) (* 4.381186 t6)) 0)
+(or (> (+ (+ (+ t3 (* 0.391934 t4)) (* 0.550236 t5)) (* 0.772476 t6)) 0) (<= (+ (- (+ t3 (* 0.509706 t4)) (* 0.713937 (* t5 (+ -0.878906 (* 0.100000 (+ (- (- (* 0.626047 t1)) (* 0.878906 t2)) (sin -0.626047))))))) (* t6 (pow (+ -0.878906 (* 0.100000 (+ (- (- (* 0.626047 t1)) (* 0.878906 t2)) (sin -0.626047)))) 2))) 0))
+(or (> (+ (+ (+ t3 (* 0.404340 t4)) (* 0.596445 t5)) (* 0.879822 t6)) 0) (<= (+ (- (+ t3 (* 0.532427 t4)) (* 0.729676 (* t5 (+ -0.937988 (* 0.100000 (+ (- (- (* 0.635877 t1)) (* 0.937988 t2)) (sin -0.635877))))))) (* t6 (pow (+ -0.937988 (* 0.100000 (+ (- (- (* 0.635877 t1)) (* 0.937988 t2)) (sin -0.635877)))) 2))) 0))
+(or (> (+ (- (+ t3 t4) (* 0.000000 t5)) (* 0.000000 t6)) 0) (<= (+ (+ (+ t3 t4) (* t5 (+ -0.000000 (* 0.100000 (+ (- t1 (* 0.000000 t2)) (sin 1)))))) (* t6 (pow (+ -0.000000 (* 0.100000 (+ (- t1 (* 0.000000 t2)) (sin 1)))) 2))) 0))
+(or (> (+ (- (+ t3 t4) (* 0.000000 t5)) (* 0.000000 t6)) 0) (<= (+ (+ (+ t3 t4) (* t5 (+ -0.000000 (* 0.100000 (+ (- t1 (* 0.000000 t2)) (sin 1)))))) (* t6 (pow (+ -0.000000 (* 0.100000 (+ (- t1 (* 0.000000 t2)) (sin 1)))) 2))) 0))
+(or (> (+ (- (+ t3 t4) (* 0.000000 t5)) (* 0.000000 t6)) 0) (<= (+ (+ (+ t3 t4) (* t5 (+ -0.000000 (* 0.100000 (+ (- t1 (* 0.000000 t2)) (sin 1)))))) (* t6 (pow (+ -0.000000 (* 0.100000 (+ (- t1 (* 0.000000 t2)) (sin 1)))) 2))) 0))
+(or (> (+ (- (+ t3 t4) (* 0.000000 t5)) (* 0.000000 t6)) 0) (<= (+ (+ (+ t3 t4) (* t5 (+ -0.000000 (* 0.100000 (+ (- t1 (* 0.000000 t2)) (sin 1)))))) (* t6 (pow (+ -0.000000 (* 0.100000 (+ (- t1 (* 0.000000 t2)) (sin 1)))) 2))) 0))
+(or (> (+ (+ (+ t3 t4) (* 0.000000 t5)) (* 0.000000 t6)) 0) (<= (+ (- (+ t3 (* 1.000000 t4)) (* 1.000000 (* t5 (+ -0.000000 (* 0.100000 (+ (- (- t1) (* 0.000000 t2)) (sin -1))))))) (* t6 (pow (+ -0.000000 (* 0.100000 (+ (- (- t1) (* 0.000000 t2)) (sin -1)))) 2))) 0))
+(or (> (+ (- (+ t3 (* 1.000000 t4)) (* 4 t5)) (* 16.000000 t6)) 0) (<= (+ (+ (+ t3 (* 0.360000 t4)) (* 0.600000 (* t5 (+ -4.000000 (* 0.100000 (+ (- (* 1.000000 t1) (* 4.000000 t2)) (sin 1.000000))))))) (* t6 (pow (+ -4.000000 (* 0.100000 (+ (- (* 1.000000 t1) (* 4.000000 t2)) (sin 1.000000)))) 2))) 0))
+(or (> (+ (- (+ t3 (* 1.000000 t4)) (* 4.000000 t5)) (* 16.000000 t6)) 0) (<= (+ (+ (+ t3 (* 0.360000 t4)) (* 0.600000 (* t5 (+ -4.000000 (* 0.100000 (+ (- (* 1.000000 t1) (* 4.000000 t2)) (sin 1.000000))))))) (* t6 (pow (+ -4.000000 (* 0.100000 (+ (- (* 1.000000 t1) (* 4.000000 t2)) (sin 1.000000)))) 2))) 0))
+(or (> (+ (- (+ t3 (* 1.000000 t4)) (* 2.000000 t5)) (* 4.000000 t6)) 0) (<= (+ (+ (+ t3 (* 0.640000 t4)) (* 0.800000 (* t5 (+ -2.000000 (* 0.100000 (+ (- (* 1.000000 t1) (* 2.000000 t2)) (sin 1.000000))))))) (* t6 (pow (+ -2.000000 (* 0.100000 (+ (- (* 1.000000 t1) (* 2.000000 t2)) (sin 1.000000)))) 2))) 0))
+(or (> (+ (- (+ t3 (* 1.000000 t4)) (* 1.618034 t5)) (* 2.618034 t6)) 0) (<= (+ (+ (+ t3 (* 0.702574 t4)) (* 0.838197 (* t5 (+ -1.618034 (* 0.100000 (+ (- (* 1.000000 t1) (* 1.618034 t2)) (sin 1.000000))))))) (* t6 (pow (+ -1.618034 (* 0.100000 (+ (- (* 1.000000 t1) (* 1.618034 t2)) (sin 1.000000)))) 2))) 0))
+(or (> (+ (- (+ t3 (* 1.000000 t4)) (* 2.414214 t5)) (* 5.828427 t6)) 0) (<= (+ (+ (+ t3 (* 0.575442 t4)) (* 0.758579 (* t5 (+ -2.414214 (* 0.100000 (+ (- (* 1.000000 t1) (* 2.414214 t2)) (sin 1.000000))))))) (* t6 (pow (+ -2.414214 (* 0.100000 (+ (- (* 1.000000 t1) (* 2.414214 t2)) (sin 1.000000)))) 2))) 0))
+(or (> (+ (+ (+ t3 (* 1.005066 t4)) (* 3.005631 t5)) (* 8.988285 t6)) 0) (<= (+ (- (+ t3 (* 1.696075 t4)) (* 1.302334 (* t5 (+ -2.998047 (* 0.100000 (+ (- (- (* 1.002530 t1)) (* 2.998047 t2)) (sin -1.002530))))))) (* t6 (pow (+ -2.998047 (* 0.100000 (+ (- (- (* 1.002530 t1)) (* 2.998047 t2)) (sin -1.002530)))) 2))) 0))
+(or (> (+ (- (+ t3 (* 1.044753 t4)) (* 0.537527 t5)) (* 0.276559 t6)) 0) (<= (+ (+ (+ t3 (* 0.940013 t4)) (* 0.969543 (* t5 (+ -0.525888 (* 0.100000 (+ (- (* 1.022131 t1) (* 0.525888 t2)) (sin 1.022131))))))) (* t6 (pow (+ -0.525888 (* 0.100000 (+ (- (* 1.022131 t1) (* 0.525888 t2)) (sin 1.022131)))) 2))) 0))
+(or (> (+ (- (+ t3 (* 1.198125 t4)) (* 0.761081 t5)) (* 0.483459 t6)) 0) (<= (+ (+ (+ t3 (* 1.050743 t4)) (* 1.025058 (* t5 (+ -0.695313 (* 0.100000 (+ (- (* 1.094589 t1) (* 0.695313 t2)) (sin 1.094589))))))) (* t6 (pow (+ -0.695313 (* 0.100000 (+ (- (* 1.094589 t1) (* 0.695313 t2)) (sin 1.094589)))) 2))) 0))
+(or (> (+ (- (+ t3 (* 1.217888 t4)) (* 3.859908 t5)) (* 12.233388 t6)) 0) (<= (+ (+ (+ t3 (* 0.568240 t4)) (* 0.753817 (* t5 (+ -3.497626 (* 0.100000 (+ (- (* 1.103579 t1) (* 3.497626 t2)) (sin 1.103579))))))) (* t6 (pow (+ -3.497626 (* 0.100000 (+ (- (* 1.103579 t1) (* 3.497626 t2)) (sin 1.103579)))) 2))) 0))
+(or (> (+ (+ (+ t3 (* 1.218265 t4)) (* 0.140590 t5)) (* 0.016224 t6)) 0) (<= (+ (- (+ t3 (* 1.246545 t4)) (* 1.116488 (* t5 (+ -0.127374 (* 0.100000 (+ (- (- (* 1.103750 t1)) (* 0.127374 t2)) (sin -1.103750))))))) (* t6 (pow (+ -0.127374 (* 0.100000 (+ (- (- (* 1.103750 t1)) (* 0.127374 t2)) (sin -1.103750)))) 2))) 0))
+(or (> (+ (- (+ t3 (* 1.266452 t4)) (* 0.885198 t5)) (* 0.618717 t6)) 0) (<= (+ (+ (+ t3 (* 1.095600 t4)) (* 1.046709 (* t5 (+ -0.786585 (* 0.100000 (+ (- (* 1.125368 t1) (* 0.786585 t2)) (sin 1.125368))))))) (* t6 (pow (+ -0.786585 (* 0.100000 (+ (- (* 1.125368 t1) (* 0.786585 t2)) (sin 1.125368)))) 2))) 0))
+(or (> (+ (- (+ t3 (* 1.624399 t4)) (* 3.784773 t5)) (* 8.818344 t6)) 0) (<= (+ (+ (+ t3 (* 0.955628 t4)) (* 0.977562 (* t5 (+ -2.969570 (* 0.100000 (+ (- (* 1.274519 t1) (* 2.969570 t2)) (sin 1.274519))))))) (* t6 (pow (+ -2.969570 (* 0.100000 (+ (- (* 1.274519 t1) (* 2.969570 t2)) (sin 1.274519)))) 2))) 0))
+(or (> (+ (- (+ t3 (* 2.214483 t4)) (* 5.749637 t5)) (* 14.928240 t6)) 0) (<= (+ (+ (+ t3 (* 1.213838 t4)) (* 1.101743 (* t5 (+ -3.863708 (* 0.100000 (+ (- (* 1.488114 t1) (* 3.863708 t2)) (sin 1.488114))))))) (* t6 (pow (+ -3.863708 (* 0.100000 (+ (- (* 1.488114 t1) (* 3.863708 t2)) (sin 1.488114)))) 2))) 0))
+(or (> (+ (+ (+ t3 (* 2.626278 t4)) (* 4.138619 t5)) (* 6.521840 t6)) 0) (<= (+ (- (+ t3 (* 3.519221 t4)) (* 1.875959 (* t5 (+ -2.553789 (* 0.100000 (+ (- (- (* 1.620580 t1)) (* 2.553789 t2)) (sin -1.620580))))))) (* t6 (pow (+ -2.553789 (* 0.100000 (+ (- (- (* 1.620580 t1)) (* 2.553789 t2)) (sin -1.620580)))) 2))) 0))
+(or (> (+ (- (+ t3 (* 2.727082 t4)) (* 6.212318 t5)) (* 14.151717 t6)) 0) (<= (+ (+ (+ t3 (* 1.626135 t4)) (* 1.275200 (* t5 (+ -3.761877 (* 0.100000 (+ (- (* 1.651388 t1) (* 3.761877 t2)) (sin 1.651388))))))) (* t6 (pow (+ -3.761877 (* 0.100000 (+ (- (* 1.651388 t1) (* 3.761877 t2)) (sin 1.651388)))) 2))) 0))
+(or (> (+ t3 (* 4.515625 t4)) 0) (<= (+ (- (+ t3 (* 4.515625 t4)) (* 0.212500 (* t5 (+ (- (* 2.125000 t1)) (sin -2.125000))))) (* 0.010000 (* t6 (pow (+ (- (* 2.125000 t1)) (sin -2.125000)) 2)))) 0))
+(or (> (+ (+ (+ t3 (* 4.515625 t4)) (* 6.375000 t5)) (* 9 t6)) 0) (<= (+ (- (+ t3 (* 5.880625 t4)) (* 2.425000 (* t5 (+ -3 (* 0.100000 (+ (- (- (* 2.125000 t1)) (* 3 t2)) (sin -2.125000))))))) (* t6 (pow (+ -3 (* 0.100000 (+ (- (- (* 2.125000 t1)) (* 3 t2)) (sin -2.125000)))) 2))) 0))
+(or (> (+ (- (+ t3 (* 10.562500 t4)) (* 10.562500 t5)) (* 10.562500 t6)) 0) (<= (+ (+ (+ t3 (* 8.555625 t4)) (* 2.925000 (* t5 (+ -3.250000 (* 0.100000 (+ (- (* 3.250000 t1) (* 3.250000 t2)) (sin 3.250000))))))) (* t6 (pow (+ -3.250000 (* 0.100000 (+ (- (* 3.250000 t1) (* 3.250000 t2)) (sin 3.250000)))) 2))) 0))
+(or (> (+ (+ (+ t3 (* 15.627197 t4)) (* 8.274397 t5)) (* 4.381186 t6)) 0) (<= (+ (- (+ t3 (* 17.325889 t4)) (* 4.162438 (* t5 (+ -2.093128 (* 0.100000 (+ (- (- (* 3.953125 t1)) (* 2.093128 t2)) (sin -3.953125))))))) (* t6 (pow (+ -2.093128 (* 0.100000 (+ (- (- (* 3.953125 t1)) (* 2.093128 t2)) (sin -3.953125)))) 2))) 0))
+(or (> (+ t3 (* 2.250000 t6)) 0) (<= (+ (- (+ t3 (* 0.022500 t4)) (* 0.150000 (* t5 (+ -1.500000 (* 0.100000 (+ (- (* 1.500000 t2)) (sin 0))))))) (* t6 (pow (+ -1.500000 (* 0.100000 (+ (- (* 1.500000 t2)) (sin 0)))) 2))) 0))
+(or (>= t1 0.200000) (>= t2 -0.800000) (>= t3 -1.800000) (>= t4 2.200000) (>= t5 -0.800000) (>= t6 1.200000) (<= t1 -0.200000) (<= t2 -1.200000) (<= t3 -2.200000) (<= t4 1.800000) (<= t5 -1.200000) (<= t6 0.800000))
+(or (>= t1 0.200000) (>= t2 0.200000) (>= t3 -2.800000) (>= t4 3.200000) (>= t5 -3.800000) (>= t6 -0.800000) (<= t1 -0.200000) (<= t2 -0.200000) (<= t3 -3.200000) (<= t4 2.800000) (<= t5 -4.200000) (<= t6 -1.200000))
+(or (>= t1 0.200000) (>= t2 0.200000) (>= t3 -0.800000) (>= t4 1.200000) (>= t5 -0.800000) (>= t6 0.200000) (<= t1 -0.200000) (<= t2 -0.200000) (<= t3 -1.200000) (<= t4 0.800000) (<= t5 -1.200000) (<= t6 -0.200000))
+(or (>= t1 0.200000) (>= t2 0.200000) (>= t3 -0.800000) (>= t4 1.200000) (>= t5 -0.800000) (>= t6 1.200000) (<= t1 -0.200000) (<= t2 -0.200000) (<= t3 -1.200000) (<= t4 0.800000) (<= t5 -1.200000) (<= t6 0.800000))
+(or (>= t1 0.200000) (>= t2 0.200000) (>= t3 1.200000) (>= t4 1.200000) (>= t5 -0.800000) (>= t6 -0.800000) (<= t1 -0.200000) (<= t2 -0.200000) (<= t3 0.800000) (<= t4 0.800000) (<= t5 -1.200000) (<= t6 -1.200000))
+(or (>= t1 0.200000) (>= t2 1.200000) (>= t3 -1.800000) (>= t4 2.200000) (>= t5 -0.800000) (>= t6 0.200000) (<= t1 -0.200000) (<= t2 0.800000) (<= t3 -2.200000) (<= t4 1.800000) (<= t5 -1.200000) (<= t6 -0.200000))
+(or (>= t1 0.200000) (>= t2 1.200000) (>= t3 -0.800000) (>= t4 1.200000) (>= t5 -0.800000) (>= t6 1.200000) (<= t1 -0.200000) (<= t2 0.800000) (<= t3 -1.200000) (<= t4 0.800000) (<= t5 -1.200000) (<= t6 0.800000))
+(or (>= t1 1.200000) (>= t2 -1.800000) (>= t3 -0.800000) (>= t4 1.200000) (>= t5 -0.800000) (>= t6 0.200000) (<= t1 0.800000) (<= t2 -2.200000) (<= t3 -1.200000) (<= t4 0.800000) (<= t5 -1.200000) (<= t6 -0.200000))
+(or (>= t1 1.200000) (>= t2 -0.800000) (>= t3 -1.800000) (>= t4 2.200000) (>= t5 -0.800000) (>= t6 0.200000) (<= t1 0.800000) (<= t2 -1.200000) (<= t3 -2.200000) (<= t4 1.800000) (<= t5 -1.200000) (<= t6 -0.200000))
+(or (>= t1 2.200000) (>= t2 1.200000) (>= t3 -1.800000) (>= t4 2.200000) (>= t5 -0.800000) (>= t6 0.200000) (<= t1 1.800000) (<= t2 0.800000) (<= t3 -2.200000) (<= t4 1.800000) (<= t5 -1.200000) (<= t6 -0.200000))
+(or (>= t1 4.200000) (>= t2 0.200000) (>= t3 -1.800000) (>= t4 4.200000) (>= t5 -3.800000) (>= t6 -1.800000) (<= t1 3.800000) (<= t2 -0.200000) (<= t3 -2.200000) (<= t4 3.800000) (<= t5 -4.200000) (<= t6 -2.200000))
+(or (>= t1 4.200000) (>= t2 1.200000) (>= t3 -2.800000) (>= t4 3.200000) (>= t5 -0.800000) (>= t6 2.200000) (<= t1 3.800000) (<= t2 0.800000) (<= t3 -3.200000) (<= t4 2.800000) (<= t5 -1.200000) (<= t6 1.800000))
+(or (>= t1 4.200000) (>= t2 1.200000) (>= t3 -1.800000) (>= t4 2.200000) (>= t5 -2.800000) (>= t6 2.200000) (<= t1 3.800000) (<= t2 0.800000) (<= t3 -2.200000) (<= t4 1.800000) (<= t5 -3.200000) (<= t6 1.800000))
+(or (>= t1 15.200000) (>= t2 -11.800000) (>= t3 -1.800000) (>= t4 14.200000) (>= t5 -4.800000) (>= t6 -1.800000) (<= t1 14.800000) (<= t2 -12.200000) (<= t3 -2.200000) (<= t4 13.800000) (<= t5 -5.200000) (<= t6 -2.200000))))
+
+(assert
+ (and
+  ;; (>= t1 -16)
+  ;; (>= t2 -16)
+  ;; (>= t3 -16)
+  ;; (>= t4 -16)
+  ;; (>= t5 -16)
+  ;; (>= t6 -16)
+  (<= t1 16)
+  ;; (<= t2 16)
+  ;; (<= t3 16)
+  ;; (<= t4 16)
+  ;; (<= t5 16)
+  ;; (<= t6 16)
+))
+
+(check-sat)
diff --git a/dreal/test/smt2/github_issue_250_plus.smt2.expected b/dreal/test/smt2/github_issue_250_plus.smt2.expected
new file mode 100644
index 00000000..a0270033
--- /dev/null
+++ b/dreal/test/smt2/github_issue_250_plus.smt2.expected
@@ -0,0 +1,1 @@
+delta-sat with delta = 0.001