Bug in egraph-explanation shortcut

src/frontend/smt2/smt2_commands.c

@@ -160,7 +160,7 @@ static void dump_bv_solver(FILE *f, bv_solver_t *solver) {
   print_bv_solver_dag(f, solver);
   if (solver->blaster != NULL) {
     fprintf(f, "\n--- Gates ---\n");
-    print_gate_table(f, &solver->blaster->htbl);
+    print_gate_table(f, solver->blaster->htbl);
   }
   fprintf(f, "\n");
 }
@@ -2872,7 +2872,13 @@ static void check_delayed_assertions(smt2_globals_t *g) {
       if (g->delegate != NULL && g->logic_code == QF_BV) {
 	status = check_with_delegate(g->ctx, g->delegate, g->verbosity);
       } else {
+	/* printf("INITIAL CONTEXT\n"); */
+	/* dump_context(stdout, g->ctx); */
+	/* printf("END\n\n"); */
 	status = check_sat_with_timeout(g, &g->parameters);
+	/* printf("\nFINAL CONTEXT\n"); */
+	/* dump_context(stdout, g->ctx); */
+	/* printf("END\n\n"); */
       }
 
       report_status(g, status);
@@ -5908,7 +5914,7 @@ void smt2_check_sat(void) {
       } else if (__smt2_globals.produce_unsat_cores) {
         delayed_assertions_unsat_core(&__smt2_globals);
       } else {
-	// show_delayed_assertions(&__smt2_globals);
+	//	show_delayed_assertions(&__smt2_globals);
 #ifndef THREAD_SAFE
         check_delayed_assertions(&__smt2_globals);
 #else

src/solvers/egraph/egraph.c

@@ -49,6 +49,7 @@
 
 #include "solvers/cdcl/smt_core_printer.h"
 #include "solvers/egraph/egraph_printer.h"
+#include "solvers/cdcl/smt_core_printer.h"
 
 #endif
 
@@ -4416,6 +4417,14 @@ static bool process_equality(egraph_t *egraph, occ_t t1, occ_t t2, int32_t i) {
     }
   }
 
+#if TRACE_FCHECK
+  printf("\nDONE PROCESSING EQUALITY\n\n");
+  print_egraph_terms(stdout, egraph);
+  printf("\n");
+  print_egraph_root_classes_details(stdout, egraph);
+  fflush(stdout);
+#endif
+
   return true;
 }
 
@@ -5259,8 +5268,8 @@ literal_t egraph_make_simple_eq(egraph_t *egraph, occ_t t1, occ_t t2) {
 /*
  * Check whether (eq t1 t2) exists and if it does return the
  * corresponding literal.
- * - return null_literal if (eq t1 t2) does not exist (or if it's not
- *   attached to a Boolean variable).
+ * - return null_literal if (eq t1 t2) does not exist
+ * - return false_literal if (eq t1 t2) does exist but is not attached to an atom
  */
 literal_t egraph_find_eq(egraph_t *egraph, occ_t t1, occ_t t2) {
   occ_t aux;
@@ -5284,7 +5293,7 @@ literal_t egraph_find_eq(egraph_t *egraph, occ_t t1, occ_t t2) {
     // null_thvar is possible if (eq t1 t2) is false at the top level
     if (v == null_thvar) {
       assert(egraph_term_is_false(egraph, eq) || egraph_term_asserted_false(egraph, eq));
-      l = true_literal; // eq is asserted as an axiom, so its literal is true
+      l = false_literal; // eq is asserted as an axiom, so its literal is false
     } else {
       l = pos_lit(v);
     }
@@ -5970,7 +5979,10 @@ static fcheck_code_t baseline_final_check(egraph_t *egraph) {
   uint32_t i, max_eq;
 
 #if TRACE_FCHECK
-  printf("---> EGRAPH: final check (baseline)\n");
+  printf("---> EGRAPH: final check (baseline)\n\n");
+  print_egraph_terms(stdout, egraph);
+  printf("\n");
+  print_egraph_root_classes_details(stdout, egraph);
   fflush(stdout);
 #endif
 
@@ -6522,12 +6534,15 @@ void egraph_propagate_equality(egraph_t *egraph, eterm_t t1, eterm_t t2, expl_ta
           egraph_term_is_function(egraph, t2)));
 
   if (egraph_equal_occ(egraph, pos_occ(t1), pos_occ(t2))) {
+#if 0
+    printf("---> EGRAPH: redundant eq prop: g!%"PRId32" == g!%"PRId32"\n", t1, t2);
+#endif
     // redundant
     return;
   }
 
 #if 0
-  printf("---> EGRAPH: good equality: g!%"PRId32" == g!%"PRId32"\n", t1, t2);
+  printf("---> EGRAPH: good eq prop: g!%"PRId32" == g!%"PRId32"\n", t1, t2);
 #endif
   egraph->stats.eq_props ++;
 

src/solvers/egraph/egraph.h

@@ -188,7 +188,7 @@ extern literal_t egraph_make_simple_eq(egraph_t *egraph, occ_t t1, occ_t t2);
 /*
  * Check whether (eq t1 t2) exists and if it does return the corresponding literal.
  * - return null_literal if (eq t1 t2) does not exist
- * - return true_literal if (eq t1 t2) does exist but is not attached to an atom
+ * - return false_literal if (eq t1 t2) does exist but is not attached to an atom
  *   (and thus not attached to a boolean variable). This may happen after a call to
  *   egraph_assert_diseq_axiom(egraph, t1, t2).
  */

src/solvers/simplex/simplex.c

@@ -11773,6 +11773,16 @@ uint32_t simplex_reconcile_model(simplex_solver_t *solver, uint32_t max_eq) {
     simplex_adjust_model(solver);
   }
 
+
+#if TRACE
+  printf("SIMPLEX: reconcile model\n");
+  print_simplex_vars(stdout, solver);
+  printf("\n");
+  print_simplex_assignment(stdout, solver);
+  printf("\n\n");
+  fflush(stdout);
+#endif
+
   init_int_hclass(&hclass, 0, solver, (iclass_hash_fun_t) simplex_model_hash,
                   (iclass_match_fun_t) simplex_var_equal_in_model);
 
@@ -11810,6 +11820,14 @@ static void simplex_prep_model(simplex_solver_t *solver) {
   if (simplex_option_enabled(solver, SIMPLEX_ADJUST_MODEL)) {
     simplex_adjust_model(solver);
   }
+#if TRACE
+  printf("SIMPLEX: prepare model\n");
+  print_simplex_vars(stdout, solver);
+  printf("\n");
+  print_simplex_assignment(stdout, solver);
+  printf("\n\n");
+  fflush(stdout);
+#endif
 }
 
 static void simplex_release_model(simplex_solver_t *solver) {