From 06cded761d4241445e7c87de52fd6ed476a2ef59 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Wed, 26 Jul 2023 08:33:26 -0500
Subject: [PATCH] Another test

---
 tests/CMakeLists.txt           |  1 +
 tests/define-const-simple.smt2 | 15 +++++++++++++++
 2 files changed, 16 insertions(+)
 create mode 100644 tests/define-const-simple.smt2

diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt
index 1985d42..ed6c726 100644
--- 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
new file mode 100644
index 0000000..5ce5785
--- /dev/null
+++ 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))