Regression

cvc5 · Oct 2, 2024 · 140ca79 · 140ca79
1 parent 7a70721
commit 140ca79
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 0 deletions.
diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt
@@ -126,6 +126,7 @@ set(ethos_test_file_list
     simple-reference.eo
     simple-quant-reference.eo
     simple-lra-reference.eo
+    overload-standalone.eo
 )
 
 if(ENABLE_ORACLES)

diff --git a/tests/overload-standalone.eo b/tests/overload-standalone.eo
@@ -0,0 +1,14 @@
+(declare-const or (-> Bool Bool Bool) :right-assoc-nil false)
+(declare-const = (-> (! Type :var T :implicit) T T Bool))
+
+(declare-const a Bool)
+(declare-const b Bool)
+
+(define singleton-list ((T Type :implicit) (f (-> T T T)) (a T)) (eo::cons f a (eo::nil f)))
+
+(declare-rule refl ((T Type) (t T))
+  :args (t)
+  :conclusion (= t t)
+)
+
+(step @p0 (= (or b) (or b)) :rule refl :args ((singleton-list or b)))