fix #4028

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/smt/seq_axioms.cpp

@@ -667,12 +667,19 @@ void seq_axioms::ensure_digit_axiom() {
 
 
 /**
-   e1 < e2 => prefix(e1, e2) or e1 = xcy e1 < e2 => prefix(e1, e2) or
-   c < d e1 < e2 => prefix(e1, e2) or e2 = xdz e1 < e2 => e1 != e2
-   !(e1 < e2) => prefix(e2, e1) or e2 = xdz !(e1 < e2) => prefix(e2,
-   e1) or d < c !(e1 < e2) => prefix(e2, e1) or e1 = xcy !(e1 = e2) or
-   !(e1 < e2) optional: e1 < e2 or e1 = e2 or e2 < e1 !(e1 = e2) or
-   !(e2 < e1) !(e1 < e2) or !(e2 < e1)
+   e1 < e2 => prefix(e1, e2) or e1 = xcy 
+   e1 < e2 => prefix(e1, e2) or c < d 
+   e1 < e2 => prefix(e1, e2) or e2 = xdz 
+   e1 < e2 => e1 != e2
+   !(e1 < e2) => prefix(e2, e1) or e2 = xdz 
+   !(e1 < e2) => prefix(e2, e1) or d < c 
+   !(e1 < e2) => prefix(e2, e1) or e1 = xcy 
+   !(e1 = e2) or !(e1 < e2) 
+
+   optional: 
+   e1 < e2 or e1 = e2 or e2 < e1 
+   !(e1 = e2) or !(e2 < e1) 
+   !(e1 < e2) or !(e2 < e1)
  */
 void seq_axioms::add_lt_axiom(expr* n) {
     expr* e1 = nullptr, *e2 = nullptr;

src/smt/theory_dense_diff_logic_def.h

@@ -41,7 +41,7 @@ namespace smt {
 
     template<typename Ext>
     theory* theory_dense_diff_logic<Ext>::mk_fresh(context * new_ctx) { 
-        return alloc(theory_dense_diff_logic<Ext>, new_ctx->get_manager(), m_params); 
+        return alloc(theory_dense_diff_logic<Ext>, new_ctx->get_manager(), new_ctx->get_fparams());
     }
 
     template<typename Ext>

src/smt/theory_diff_logic_def.h

@@ -492,7 +492,7 @@ template<typename Ext>
 void theory_diff_logic<Ext>::propagate() {
     if (m_params.m_arith_adaptive) {
 
-        switch(m_params.m_arith_propagation_strategy) {
+        switch (m_params.m_arith_propagation_strategy) {
 
         case ARITH_PROP_PROPORTIONAL: {
 
@@ -528,6 +528,8 @@ void theory_diff_logic<Ext>::propagate() {
             break;
         }
         default:
+            std::cout << m_params.m_arith_propagation_strategy << "\n";
+            SASSERT(false);
             UNREACHABLE();
             propagate_core();
         }
@@ -1416,7 +1418,7 @@ bool theory_diff_logic<Ext>::internalize_objective(expr * n, rational const& m,
 
 template<typename Ext>
 theory* theory_diff_logic<Ext>::mk_fresh(context* new_ctx) {
-    return alloc(theory_diff_logic<Ext>, new_ctx->get_manager(), m_params); 
+    return alloc(theory_diff_logic<Ext>, new_ctx->get_manager(), new_ctx->get_fparams());
 }
 
 template<typename Ext>