-// void testBasicConflict() {
-// Node x = d_nm->mkVar(*d_realType);
-// Node c = d_nm->mkConst<Rational>(d_zero);
-//
-// Node eq = d_nm->mkNode(EQUAL, x, c);
-// Node lt = d_nm->mkNode(NOT, d_nm->mkNode(GEQ, x, c));
-// Node expectedDisjunct = simulateSplit(x,c);
-//
-// fakeTheoryEnginePreprocess(eq);
-// fakeTheoryEnginePreprocess(lt);
-//
-// d_arith->assertFact(eq);
-// d_arith->assertFact(lt);
-//
-// d_arith->check(d_level);
-//
-// TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 2u);
-// TS_ASSERT_EQUALS(d_outputChannel.getIthNode(0), expectedDisjunct);
-// TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), AUG_LEMMA);
-//
-// TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), CONFLICT);
-//
-// Node expectedClonflict = d_nm->mkNode(AND, eq, lt);
-//
-// TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), expectedClonflict);
-// }
-
-// void testBasicPropagate() {
-// Node x = d_nm->mkVar(*d_realType);
-// Node c = d_nm->mkConst<Rational>(d_zero);
-//
-// Node eq = d_nm->mkNode(EQUAL, x, c);
-// Node lt = d_nm->mkNode(NOT, d_nm->mkNode(GEQ, x, c));
-// Node expectedDisjunct = simulateSplit(x,c);
-//
-// fakeTheoryEnginePreprocess(eq);
-// fakeTheoryEnginePreprocess(lt);
-//
-// d_arith->assertFact(eq);
-//
-//
-// d_arith->check(d_level);
-// d_arith->propagate(d_level);
-//
-// TS_ASSERT_EQUALS(d_outputChannel.getNumCalls(), 2u);
-// TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(0), AUG_LEMMA);
-//
-//
-// Node expectedProp = d_nm->mkNode(GEQ, x, c);
-// TS_ASSERT_EQUALS(d_outputChannel.getIthCallType(1), PROPAGATE);
-// TS_ASSERT_EQUALS(d_outputChannel.getIthNode(1), expectedProp);
-//
-// }