Fix #332

Minor correction to Boolean quantified variable instantiation

src/solvers/quant/quant_solver.c

@@ -501,6 +501,7 @@ static term_t term_substitution(quant_solver_t *solver, term_t *var, term_t *val
   int_hmap_pair_t *p;
   uint32_t i;
   term_t x;
+  term_t val;
 
   subst.mngr = solver->prob->manager;
   subst.terms = solver->prob->terms;
@@ -511,8 +512,13 @@ static term_t term_substitution(quant_solver_t *solver, term_t *var, term_t *val
 
   for (i=0; i<n; i++) {
     x = var[i];
+    val = value[i];
+    if (is_neg_term(x)) {
+      x = opposite_term(x);
+      val = opposite_term(val);
+    }
     p = int_hmap_get(&subst.map, x);
-    p->val = value[i];
+    p->val = val;
 
     assert(is_pos_term(x));
     assert(good_term(subst.terms, x));

tests/regress/efsmt/ematch/issue332.smt2

@@ -0,0 +1,6 @@
+(set-logic UF)
+(declare-fun uf4_2 (Bool Bool Bool Bool) Bool)
+(declare-fun uf7_2 (Bool Bool Bool Bool Bool Bool Bool) Bool)
+(assert (uf7_2 true (not (exists ((q0 Bool) (q1 Bool) (q2 Bool) (q3 Bool)) q2)) true true true true true))
+(assert (uf4_2 true true true true))
+(check-sat)

tests/regress/efsmt/ematch/issue332.smt2.gold

@@ -0,0 +1 @@
+sat