Another test

cvc5 · Jul 26, 2023 · 06cded7 · 06cded7
1 parent f178e48
commit 06cded7
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 0 deletions.
diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt
@@ -22,6 +22,7 @@ set(alfc_test_file_list
     substitution.smt2
     substitution-binary-only.smt2
     beta-reduce-define-fun.smt2
+    define-const-simple.smt2
 )
 
 macro(alfc_test file)

diff --git a/tests/define-const-simple.smt2 b/tests/define-const-simple.smt2
@@ -0,0 +1,15 @@
+
+(declare-const true Bool)
+(declare-const false Bool)
+(declare-const not (-> Bool Bool))
+
+(define-const f_true Bool true)
+
+
+(declare-rule trust ((f Bool))
+   :premises ()
+   :args (f)
+   :conclusion f
+)
+
+(step a1 true :rule trust :args (f_true))