1 files changed, 22 insertions, 0 deletions
diff --git a/test/regress/regress0/difficulty-model-ex.smt2 b/test/regress/regress0/difficulty-model-ex.smt2
new file mode 100644
index 000000000..0546b5118
--- /dev/null
+++ b/test/regress/regress0/difficulty-model-ex.smt2
@@ -0,0 +1,22 @@
+; COMMAND-LINE: --produce-difficulty --difficulty-mode=model-check
+; SCRUBBER: sed 's/.*//g'
+; EXIT: 0
+
+(set-logic ALL)
+(set-option :produce-difficulty true)
+(declare-fun P (Int) Bool)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(declare-fun z () Int)
+
+(assert (= z 78))
+
+(assert (! (= (* x x) z) :named a1))
+
+(assert (= y 0))
+
+(assert (P y))
+
+(check-sat)
+
+(get-difficulty)