Finish implementing the symbolic case of switch evaluation

1 files changed, 9 insertions, 3 deletions

diff --git a/src/Synthesis.ml b/src/Synthesis.ml
index 9ce6c8da..51aa0882 100644
--- a/src/Synthesis.ml
+++ b/src/Synthesis.ml
@@ -33,13 +33,19 @@ let synthesize_symbolic_expansion_no_branching (sv : V.symbolic_value)
     (see : symbolic_expansion) : unit =
   ()
 
-(** Synthesize code for a symbolic expansion which leads to branching
-    (for instance when evaluating the discriminant of a symbolic value).
+(** Synthesize code for a symbolic enum expansion (which leads to branching)
  *)
-let synthesize_symbolic_expansion_branching (sv : V.symbolic_value)
+let synthesize_symbolic_expansion_enum_branching (sv : V.symbolic_value)
     (seel : symbolic_expansion list) : unit =
   ()
 
+let synthesize_symbolic_expansion_if_branching (sv : V.symbolic_value) : unit =
+  ()
+
+let synthesize_symbolic_expansion_switch_int_branching (sv : V.symbolic_value) :
+    unit =
+  ()
+
 let synthesize_unary_op (unop : E.unop) (op : V.typed_value)
     (dest : V.symbolic_value) : unit =
   ()