fix #4790

src/cmd_context/cmd_context.cpp

@@ -336,6 +336,10 @@ bool cmd_context::macros_find(symbol const& s, unsigned n, expr*const* args, exp
                 coerced_args.push_back(au.mk_to_real(args[i]));
                 continue;
             }
+            if (au.is_int(d.m_domain[i]) && au.is_real(args[i])) {
+                coerced_args.push_back(au.mk_to_int(args[i]));
+                continue;
+            }
             eq = false;
         }
         if (eq) {
@@ -1864,6 +1868,7 @@ void cmd_context::validate_model() {
         cancel_eh<reslimit> eh(m().limit());
         expr_ref r(m());
         scoped_ctrl_c ctrlc(eh);
+        expr_mark seen;
         bool invalid_model = false;
         for (expr * a : assertions()) {
             if (is_ground(a)) {
@@ -1888,7 +1893,7 @@ void cmd_context::validate_model() {
                     continue;
                 }
 
-                analyze_failure(evaluator, a, true);
+                analyze_failure(seen, evaluator, a, true);
                 IF_VERBOSE(11, model_smt2_pp(verbose_stream(), *this, *md, 0););                
                 TRACE("model_validate", model_smt2_pp(tout, *this, *md, 0););
                 invalid_model |= m().is_false(r);
@@ -1900,56 +1905,59 @@ void cmd_context::validate_model() {
     }
 }
 
-void cmd_context::analyze_failure(model_evaluator& ev, expr* a, bool expected_value) {
+void cmd_context::analyze_failure(expr_mark& seen, model_evaluator& ev, expr* a, bool expected_value) {
     expr* c = nullptr, *t = nullptr, *e = nullptr;
+    if (seen.is_marked(a))
+        return;
+    seen.mark(a, true);
     if (m().is_not(a, e)) {
-        analyze_failure(ev, e, !expected_value);
+        analyze_failure(seen, ev, e, !expected_value);
         return;
     }
     if (!expected_value && m().is_or(a)) {
         for (expr* arg : *to_app(a)) {
             if (ev.is_true(arg)) {
-                analyze_failure(ev, arg, false);
+                analyze_failure(seen, ev, arg, false);
                 return;
             }
         }
     }
     if (expected_value && m().is_and(a)) {
         for (expr* arg : *to_app(a)) {
             if (ev.is_false(arg)) {
-                analyze_failure(ev, arg, true);
+                analyze_failure(seen, ev, arg, true);
                 return;
             }
         }
     }
     if (expected_value && m().is_ite(a, c, t, e)) {
         if (ev.is_true(c) && ev.is_false(t)) {
-            if (!m().is_true(c)) analyze_failure(ev, c, false);
-            if (!m().is_false(t)) analyze_failure(ev, t, true);
+            if (!m().is_true(c)) analyze_failure(seen, ev, c, false);
+            if (!m().is_false(t)) analyze_failure(seen, ev, t, true);
             return;
         }
         if (ev.is_false(c) && ev.is_false(e)) {
-            if (!m().is_false(c)) analyze_failure(ev, c, true);
-            if (!m().is_false(e)) analyze_failure(ev, e, true);
+            if (!m().is_false(c)) analyze_failure(seen, ev, c, true);
+            if (!m().is_false(e)) analyze_failure(seen, ev, e, true);
             return;
         }
     }
     if (!expected_value && m().is_ite(a, c, t, e)) {
         if (ev.is_true(c) && ev.is_true(t)) {
-            if (!m().is_true(c)) analyze_failure(ev, c, false);
-            if (!m().is_true(t)) analyze_failure(ev, t, false);
+            if (!m().is_true(c)) analyze_failure(seen, ev, c, false);
+            if (!m().is_true(t)) analyze_failure(seen, ev, t, false);
             return;
         }
         if (ev.is_false(c) && ev.is_true(e)) {
-            if (!m().is_false(c)) analyze_failure(ev, c, true);
-            if (!m().is_true(e)) analyze_failure(ev, e, false);
+            if (!m().is_false(c)) analyze_failure(seen, ev, c, true);
+            if (!m().is_true(e)) analyze_failure(seen, ev, e, false);
             return;
         }
     }
-    IF_VERBOSE(10, verbose_stream() << "model check failed on: " << " " << mk_pp(a, m()) << "\n";);                
-    IF_VERBOSE(10, verbose_stream() << "expected value: " << (expected_value?"true":"false") << "\n";);                
+    IF_VERBOSE(10, verbose_stream() << "#" << a->get_id() << " " << mk_pp(a, m()) << " expected: "
+               << (expected_value?"true":"false") << "\n";);                
 
-    IF_VERBOSE(10, display_detailed_analysis(verbose_stream(), ev, a));
+    IF_VERBOSE(11, display_detailed_analysis(verbose_stream(), ev, a));
 }
 
 void cmd_context::display_detailed_analysis(std::ostream& out, model_evaluator& ev, expr* e) {

src/cmd_context/cmd_context.h

@@ -368,7 +368,7 @@ class cmd_context : public progress_callback, public tactic_manager, public ast_
     check_sat_state cs_state() const;
     void complete_model(model_ref& mdl) const;
     void validate_model();
-    void analyze_failure(model_evaluator& ev, expr* e, bool expected_value);
+    void analyze_failure(expr_mark& seen, model_evaluator& ev, expr* e, bool expected_value);
     void display_detailed_analysis(std::ostream& out, model_evaluator& ev, expr* e);
     void display_model(model_ref& mdl);