fix: z3 bug where known variables were interpreted as "known"

sillydan1 · Sep 14, 2022 · f3430b0 · f3430b0
1 parent 29cbe74
commit f3430b0
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/drivers/z3_driver.cpp b/src/drivers/z3_driver.cpp
@@ -104,6 +104,8 @@ namespace expr {
     }
 
     auto z3_driver::as_z3_expression(const identifier_t& ref) -> z3::expr {
+        if(known.contains(ref.ident))
+            return as_z3_expression(known.at(ref.ident));
         auto it = find(ref.ident);
         return std::visit(ya::overload(
                 [this, &ref](const int& _)          { return c.int_const(ref.ident.c_str()); },