diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,7 +1,11 @@
 # Revision history for package `eflint` 
 
-## 3.1.0.0 (2023/05/22)  
+## 3.1.0.0 (2023/04/22)  
 
 * Started using changelog.
 
-Last significant update: inclusion of 'instance queries' of the form `?- <EXPR>.` 
+Last significant update: inclusion of 'instance queries' of the form `?- <EXPR>.`
+
+## 3.1.0.1 (2023/04/24)
+
+Added an additional form of instance query of the form `?-- <EXPR>.` as syntactic sugar for `?- <EXPR> When Holds(<EXPR>).`
diff --git a/eflint.cabal b/eflint.cabal
--- a/eflint.cabal
+++ b/eflint.cabal
@@ -1,7 +1,7 @@
 cabal-version:       >=1.10
 
 name:                eflint 
-version:             3.1.0.0
+version:             3.1.0.1
 synopsis:            Simulation interpreter for FLINT policy descriptions
 description:
 
diff --git a/src/Language/EFLINT/Interpreter.hs b/src/Language/EFLINT/Interpreter.hs
--- a/src/Language/EFLINT/Interpreter.hs
+++ b/src/Language/EFLINT/Interpreter.hs
@@ -128,8 +128,11 @@
                  let queryRes | all (== (ResBool True)) vs = QuerySuccess
                               | otherwise                  = QueryFailure
                  tell [QueryRes queryRes] >> no_effect
-  CInstQuery vs t -> error_or_process (foreach vs (whenTagged (eval (When t (Present t))) return)) spec state inpm $ \vs -> 
-                      do tell [InstQueryRes (concat vs)] >> no_effect
+  CInstQuery b vs t -> 
+    let t' | b         = When t (Present t)
+           | otherwise = t
+    in error_or_process (foreach vs (whenTagged (eval t') return)) spec state inpm $ \vs -> 
+                      tell [InstQueryRes (concat vs)] >> no_effect
   CCreate vs t    -> single_effect (CAll vs t)
   CTerminate vs t -> single_effect (TAll vs t)
   CObfuscate vs t -> single_effect (OAll vs t)
diff --git a/src/Language/EFLINT/Parse.hs b/src/Language/EFLINT/Parse.hs
--- a/src/Language/EFLINT/Parse.hs
+++ b/src/Language/EFLINT/Parse.hs
@@ -20,7 +20,7 @@
                 , "Atom", "String", "Int", "Time", "Current Time"
                 , "Exists", "Forall", "Foreach", "Force"
                 , "Extend", "Event", "Act", "Fact", "Physical", "Bool", "Var", "Function", "Invariant", "Predicate", "Duty", "Actor", "Holder", "Claimant", "Recipient", "Related to", "Conditioned by", "Creates", "Terminates", "Obfuscates", "Terminated by", "Created by", "With" , "Identified by", "Derived from", "Derived externally", "Enforced by", "Syncs with"
-                , "Do", "Placeholder", "For", "Not", "Open", "Closed", "?-" 
+                , "Do", "Placeholder", "For", "Not", "Open", "Closed", "?-", "?--" 
                 , "#", "##", "###", "####"
                 , "#include", "#require"
                 ]
@@ -495,6 +495,7 @@
   <||> keychar '~'  **> opt_foreach Obfuscate 
   <||> PQuery <$$ keychar '?'  <**> value_expr 
   <||> PQuery . Not <$$ keyword "!?"  <**> value_expr 
-  <||> keyword "?-" **> opt_foreach PInstQuery 
+  <||> keyword "?-" **> opt_foreach (PInstQuery False)
+  <||> keyword "?--" **> opt_foreach (PInstQuery True)
   <||> PDeclBlock <$$> declarations 
 
diff --git a/src/Language/EFLINT/Print.hs b/src/Language/EFLINT/Print.hs
--- a/src/Language/EFLINT/Print.hs
+++ b/src/Language/EFLINT/Print.hs
@@ -16,9 +16,11 @@
 ppPhrase :: Phrase -> String
 ppPhrase p = case p of
   PQuery t          -> "?" ++ ppTerm t
-  PInstQuery vs t 
-    | null vs       -> "?-" ++ ppTerm t
-    | otherwise     -> "?-" ++ foreach vs (ppTerm t)
+  PInstQuery b vs t 
+    | null vs       -> keyw ++ ppTerm t
+    | otherwise     -> keyw ++ foreach vs (ppTerm t)
+   where keyw | b         = "?--"
+              | otherwise = "?-"
   PDo t             -> ppTagged t
   PTrigger vs t     -> foreach vs $ ppTerm t
   Create vs t       -> "+" ++ foreach vs (ppTerm t)
@@ -40,9 +42,11 @@
   CTerminate vs t -> "-" ++ foreach vs (ppTerm t)
   CObfuscate vs t -> "~" ++ foreach vs (ppTerm t)
   CQuery t        -> "?" ++ ppTerm t
-  CInstQuery vs t 
-    |null vs      -> "?-" ++ ppTerm t
-    |otherwise    -> "?-" ++ foreach vs (ppTerm t)
+  CInstQuery b vs t 
+    |null vs      -> keyw ++ ppTerm t
+    |otherwise    -> keyw ++ foreach vs (ppTerm t)
+   where keyw | b         = "?--"
+              | otherwise = "?-"
   CPDir dir       -> case dir of
    DirInv ty      -> "Invariant " ++ ty   
 
diff --git a/src/Language/EFLINT/Spec.hs b/src/Language/EFLINT/Spec.hs
--- a/src/Language/EFLINT/Spec.hs
+++ b/src/Language/EFLINT/Spec.hs
@@ -185,7 +185,7 @@
             | Terminate [Var] Term
             | Obfuscate [Var] Term
             | PQuery Term
-            | PInstQuery [Var] Term
+            | PInstQuery Bool {- whether requested instances must hold true -} [Var] Term
             | PDeclBlock [Decl]
             | PSkip
             deriving (Eq, Show, Read)
@@ -275,7 +275,7 @@
              | CTerminate [Var] Term
              | CObfuscate [Var] Term
              | CQuery Term
-             | CInstQuery [Var] Term
+             | CInstQuery Bool {- whether generated instances must be present -} [Var] Term
              | CPOnlyDecls
              | CPDir CDirective
              | CSeq CPhrase CPhrase
diff --git a/src/Language/EFLINT/StaticEval.hs b/src/Language/EFLINT/StaticEval.hs
--- a/src/Language/EFLINT/StaticEval.hs
+++ b/src/Language/EFLINT/StaticEval.hs
@@ -120,10 +120,10 @@
   Terminate vs t    -> fmap (de_stmt p) (compile_stmt (to_stmt p))
   Obfuscate vs t    -> fmap (de_stmt p) (compile_stmt (to_stmt p))
   PQuery t          -> fmap (de_stmt p) (compile_stmt (to_stmt p))
-  PInstQuery vs t   -> do
+  PInstQuery b vs t   -> do
     fs <- free_vars t
     let unbounds = S.toList (fs `S.difference` S.fromList vs)
-    CInstQuery (vs ++ unbounds) . fst <$> compile_term t
+    CInstQuery b (vs ++ unbounds) . fst <$> compile_term t
   PDeclBlock ds     -> do
     -- introduce new types first
     let (type_decls, others) = partition isInitialTypeDecl ds