From f4d031742d969c689d38c0756a5026a434ef89b3 Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Sun, 29 Jun 2014 18:44:40 -0400
Subject: sets: "insert" operator
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

new™! support for (insert (X (Set X)) (Set X) :right-associative)
from the finte sets theory prosoal.

e.g., (insert 1 2 3 4 (singleton 5))
---
 test/regress/regress0/sets/Makefile.am | 1 +
 1 file changed, 1 insertion(+)

(limited to 'test/regress/regress0/sets/Makefile.am')

diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index ccedc7596..9536dfac1 100644
--- a/test/regress/regress0/sets/Makefile.am
+++ b/test/regress/regress0/sets/Makefile.am
@@ -44,6 +44,7 @@ TESTS =	\
 	error1.smt2 \
 	error2.smt2 \
 	eqtest.smt2 \
+	insert.smt2 \
 	fuzz14418.smt2 \
 	fuzz15201.smt2 \
 	fuzz31811.smt2 \
-- 
cgit v1.2.3