1 files changed, 31 insertions, 0 deletions
diff --git a/test/regress/regress1/difficulty-polarity.smt2 b/test/regress/regress1/difficulty-polarity.smt2
new file mode 100644
index 000000000..ce2388c54
--- /dev/null
+++ b/test/regress/regress1/difficulty-polarity.smt2
@@ -0,0 +1,31 @@
+; COMMAND-LINE: --produce-difficulty
+; SCRUBBER: sed 's/.*//g'
+; EXIT: 0
+
+(set-logic ALL)
+(set-option :finite-model-find true)
+(set-option :mbqi none)
+(set-option :produce-difficulty true)
+
+(declare-sort U 0)
+(declare-fun a () U)
+(declare-fun b () U)
+(declare-fun c () U)
+(assert (distinct a b c))
+(declare-fun P (U U) Bool)
+(declare-fun R (U) Bool)
+(declare-fun S (U) Bool)
+
+(define-fun Q () Bool (forall ((x U) (y U)) (P x y)))
+
+(assert (or (not Q) (S a)))
+(assert (R a))
+(assert (=> (R a) Q))
+
+; This example will instantiate the quantified formula 9 times, hence the
+; explanation for why it is relevant will be incremented by 9.
+; The explanation for why Q is relevant should be (=> (R b) Q) and 
+; not (or (not Q) (S a)), since the former is the reason it is asserted true.
+
+(check-sat)
+(get-difficulty)