Minor clean up

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 435abc56802a1fcb6f48d690794ea2ffbf612031..6a53cb3ab902ba012482de9e7cc7c54eb10402e4 100644 (file)
--- 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 (file)
index 921991f..0000000
--- 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)