filter out terms that are not solved

Author: NikolajBjorner

src/api/api_qe.cpp

@@ -95,10 +95,11 @@ extern "C"
 
         obj_map<ast, ast*> &map_z3 = to_ast_map_ref(map);
 
-        for (auto& kv : emap) {
-            m.inc_ref(kv.m_key);
-            m.inc_ref(kv.m_value);
-            map_z3.insert(kv.m_key, kv.m_value);
+        for (auto& [k,v] : emap) {
+            SASSERT(v);
+            m.inc_ref(k);
+            m.inc_ref(v);
+            map_z3.insert(k, v);
         }
 
         return of_expr (result);

src/api/api_solver.cpp

@@ -995,9 +995,11 @@ extern "C" {
         _terms.reset();
         _guards.reset();
         for (solver::solution const& s : solutions) {
+            if (!s.term)
+                continue;
             _vars.push_back(s.var);
             _terms.push_back(s.term);
-            _guards.push_back(s.guard);
+            _guards.push_back(s.guard ? s.guard : m.mk_true());
         }
         Z3_CATCH;
     }