From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Fri, 6 Feb 2015 00:42:08 +0000 (-0600)
Subject: Minor clean up
X-Git-Tag: cvc5-1.0.0~6399
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fca6fd532abda44c4da48d5c167b77600690e221;p=cvc5.git

Minor clean up
---

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 435abc568..6a53cb3ab 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -852,7 +852,7 @@ Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, std::map< Node
           itMap = constantReps.find(m->d_equalityEngine->getRepresentative(ri));
           if (itMap != constantReps.end()) {
             ri = (*itMap).second;
-	          recurse = false;
+            recurse = false;
           }
           else if (!evalOnly) {
             recurse = false;
diff --git a/test/regress/regress0/strings/cardinality.smt2 b/test/regress/regress0/strings/cardinality.smt2
deleted file mode 100644
index 921991f74..000000000
--- a/test/regress/regress0/strings/cardinality.smt2
+++ /dev/null
@@ -1,23 +0,0 @@
-(set-logic QF_S)
-(set-info :status unsat)
-;this option for experts only
-(set-option :strings-alphabet-card 2)
-
-(declare-fun x () String)
-(declare-fun y () String)
-(declare-fun z () String)
-(declare-fun w () String)
-(declare-fun i () Int)
-
-(assert (= i 1))
-(assert (= (str.len x) i))
-(assert (= (str.len y) i))
-(assert (= (str.len z) i))
-(assert (= (str.len w) 2))
-
-(assert (not (=  x y)))
-(assert (not (=  x z)))
-(assert (not (=  z y)))
-
-
-(check-sat)