1 files changed, 42 insertions, 0 deletions
diff --git a/test/regress/regress2/strings/pfnew-policy_variable.smt2 b/test/regress/regress2/strings/pfnew-policy_variable.smt2
new file mode 100644
index 000000000..5f24c7d59
--- /dev/null
+++ b/test/regress/regress2/strings/pfnew-policy_variable.smt2
@@ -0,0 +1,42 @@
+; COMMAND-LINE: --strings-exp --re-elim --proof-new
+; EXPECT: unsat
+(set-info :smt-lib-version 2.6)
+(set-logic ALL)
+(set-info :status unsat)
+(set-option :strings-exp true)
+(set-option :re-elim true)
+(declare-const actionName String)
+(declare-const actionNamespace String)
+(declare-const example_key String)
+
+; Action: p0.0
+(declare-const p0.0.action Bool)
+(assert (= p0.0.action (and (= "foobar" actionNamespace) (and (str.prefixof "ab" actionName) (str.contains (str.substr actionName 2 (- (str.len actionName) 3)) "b") (str.suffixof "b" actionName) (not (= actionName "abb")) (not (= actionName "ab"))))))
+
+; Policy: 0
+(declare-const p0.denies Bool)
+(assert (not p0.denies))
+(declare-const p0.allows Bool)
+(assert (= p0.allows (and (not p0.denies) p0.0.action)))
+(declare-const p0.neutral Bool)
+(assert (= p0.neutral (and (not p0.allows) (not p0.denies))))
+
+; Action: p1.0
+(declare-const p1.0.action Bool)
+(assert (= p1.0.action (and (= "foobar" actionNamespace) (and (str.prefixof "a" actionName) (str.prefixof example_key (str.substr actionName 1 (- (str.len actionName) 1))) (str.contains (str.substr actionName (+ 1 (str.len example_key)) (- (str.len actionName) 1 (str.len example_key))) "b") (str.suffixof "b" actionName)))))
+
+(declare-const p1.0.condition Bool)
+(assert (= p1.0.condition (str.prefixof "bb" example_key)))
+
+; Policy: 1
+(declare-const p1.denies Bool)
+(assert (not p1.denies))
+(declare-const p1.allows Bool)
+(assert (= p1.allows (and (not p1.denies) p1.0.action p1.0.condition)))
+(declare-const p1.neutral Bool)
+(assert (= p1.neutral (and (not p1.allows) (not p1.denies))))
+
+; Goals
+(assert (or p0.neutral p0.denies))
+(assert p1.allows)
+(check-sat)