Merge branch 'unstable' of https://github.com/Z3Prover/z3 into unstable

src/ast/fpa/fpa2bv_converter.cpp

@@ -1018,9 +1018,11 @@ void fpa2bv_converter::mk_rem(func_decl * f, unsigned num, expr * const * args,
                                   m_bv_util.mk_numeral(0, 3));
     res_exp = m_bv_util.mk_sign_extend(2, b_exp);
     
+    // CMW: Actual rounding is not necessary here, this is 
+    // just convenience to get rid of the extra bits.
     expr_ref rm(m);
-    rm = m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3);
+    rm = m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3);    
-    round(f->get_range(), rm, res_sgn, res_sig, res_exp, v7);
+    round(f->get_range(), rm, res_sgn, res_sig, res_exp, v7); 
 
     // And finally, we tie them together.        
     mk_ite(c6, v6, v7, result);
@@ -1030,6 +1032,11 @@ void fpa2bv_converter::mk_rem(func_decl * f, unsigned num, expr * const * args,
     mk_ite(c2, v2, result, result);
     mk_ite(c1, v1, result, result);
 
+    expr_ref result_is_zero(m), zeros(m);
+    mk_is_zero(result, result_is_zero);
+    mk_ite(x_is_pos, pzero, nzero, zeros);
+    mk_ite(result_is_zero, zeros, result, result);
+
     SASSERT(is_well_sorted(m, result));
 
     TRACE("fpa2bv_rem", tout << "REM = " << mk_ismt2_pp(result, m) << std::endl; );

src/interp/iz3mgr.h

@@ -279,6 +279,12 @@ class iz3mgr  {
             res[i] = arg(t,i);
     }
 
+    std::vector<ast> args(const ast &t){
+        std::vector<ast> res;
+        get_args(t,res);
+        return res;
+    }
+
     symb sym(ast t){
         raw_ast *_ast = t.raw();
         return is_app(_ast) ? to_app(_ast)->get_decl() : 0;

src/interp/iz3proof_itp.cpp

@@ -2215,8 +2215,12 @@ class iz3proof_itp_impl : public iz3proof_itp {
         }
         else {
             if(get_term_type(p) == LitA){
-                if(get_term_type(q) == LitA)
+                if(get_term_type(q) == LitA){
-                    itp = mk_false();
+                    if(op(q) == Or)
+                        itp = make_assumption(rng.hi,args(q));
+                    else 
+                        itp = mk_false();
+                }
                 else {
                     if(get_term_type(p_eq_q) == LitA)
                         itp = q;

src/interp/iz3translate.cpp

@@ -1702,14 +1702,16 @@ public:
                     return res;
                 }
             }
-            if(dk == PR_MODUS_PONENS && expect_clause && op(con) == Or){
+            if(dk == PR_MODUS_PONENS && expect_clause && op(con) == Or && op(conc(prem(proof,0))) == Or){
                 Iproof::node clause = translate_main(prem(proof,0),true);
                 res = RewriteClause(clause,prem(proof,1));
                 return res;
             }
 
+#if 0
             if(dk == PR_MODUS_PONENS && expect_clause && op(con) == Or)
                 std::cout << "foo!\n";
+#endif
 
             // no idea why this shows up
             if(dk == PR_MODUS_PONENS_OEQ){
@@ -1965,6 +1967,16 @@ public:
                 res = make(commute,pf,comm_equiv);
                 break;
             }
+            case PR_AND_ELIM: {
+                std::vector<ast> rule_ax, res_conc;
+                ast piv = conc(prem(proof,0));
+                rule_ax.push_back(make(Not,piv));
+                rule_ax.push_back(con);
+                ast pf = iproof->make_axiom(rule_ax);
+                res_conc.push_back(con);
+                res = iproof->make_resolution(piv,res_conc,pf,args[0]);
+                break;
+            }
             default:
                 pfgoto(proof);
                 assert(0 && "translate_main: unsupported proof rule");

src/util/trace.cpp

@@ -23,8 +23,8 @@ Revision History:
 std::ofstream tout(".z3-trace"); 
 #endif
 
-bool g_enable_all_trace_tags = false;
+static bool g_enable_all_trace_tags = false;
-str_hashtable* g_enabled_trace_tags = 0;
+static str_hashtable* g_enabled_trace_tags = 0;
 
 static str_hashtable& get_enabled_trace_tags() {
     if (!g_enabled_trace_tags) {