diff --git a/src/OcamlSTP/OcamlSTP.ml b/src/OcamlSTP/OcamlSTP.ml
--- a/src/OcamlSTP/OcamlSTP.ml
+++ b/src/OcamlSTP/OcamlSTP.ml
@@ -81,7 +81,7 @@
 external vc_query : context -> ([`bool], [<`expr|`const|`var]) expr -> validity = "OcamlSTP_vc_query"
 
 external vc_get_asserts : context -> ([`bool], [>`expr]) expr list = "OcamlSTP_vc_get_asserts"
-external vc_get_counterexample : context -> ('a, [<`var]) expr -> ('a, [>`const]) expr option = "OcamlSTP_vc_get_counterexample"
+external vc_get_counterexample : context -> ([<`bool|`bv] as 'a, [<`expr|`const|`var]) expr -> ('a, [>`const]) expr option = "OcamlSTP_vc_get_counterexample"
 
 external bv_width : context -> ([`bv], [<`expr|`const|`var]) expr -> int = "OcamlSTP_bv_width"
 external array_value_width : context -> ([`array], [<`expr|`const|`var]) expr -> int = "OcamlSTP_array_value_width"
diff --git a/src/OcamlSTP/OcamlSTP.mli b/src/OcamlSTP/OcamlSTP.mli
--- a/src/OcamlSTP/OcamlSTP.mli
+++ b/src/OcamlSTP/OcamlSTP.mli
@@ -228,8 +228,8 @@
 (** [vc_get_asserts stp] get the current list of assertions in the STP context [stp]. *)
 external vc_get_asserts : context -> ([`bool], [>`expr]) expr list = "OcamlSTP_vc_get_asserts"
 
-(** [vc_get_counterexample stp var] returns [Some x] where [x] is the counterexample value for the variable [var] if the previous query is [Invalid], or [None] if the previous query is [Valid]. *)
-external vc_get_counterexample : context -> ('a, [<`var]) expr -> ('a, [>`const]) expr option = "OcamlSTP_vc_get_counterexample"
+(** [vc_get_counterexample stp expr] returns [Some x] where [x] is the counterexample value for the boolean or bitvector expression [expr] if the previous query is [Invalid], or [None] if the previous query is [Valid]. *)
+external vc_get_counterexample : context -> ([<`bool|`bv] as 'a, [<`expr|`const|`var]) expr -> ('a, [>`const]) expr option = "OcamlSTP_vc_get_counterexample"
 
 
 (** {2 Metadata query} *)