[SMTChecker] Support return in CHC

Changelog.md

@@ -11,6 +11,7 @@ Compiler Features:
  * SMTChecker: Support named arguments in function calls.
  * SMTChecker: Support struct constructor.
  * SMTChecker: Support getters.
+ * SMTChecker: Support early returns in the CHC engine.
 
 Bugfixes:
  * Code generator: Do not pad empty string literals with a single 32-byte zero field in the ABI coder v1.

libsolidity/formal/CHC.cpp

@@ -202,7 +202,7 @@ bool CHC::visit(FunctionDefinition const& _function)
 
 	initFunction(_function);
 
-	auto functionEntryBlock = createBlock(m_currentFunction, PredicateType::FunctionEntry);
+	auto functionEntryBlock = createBlock(m_currentFunction, PredicateType::FunctionBlock);
 	auto bodyBlock = createBlock(&m_currentFunction->body(), PredicateType::FunctionBlock);
 
 	auto functionPred = predicate(*functionEntryBlock);
@@ -469,6 +469,8 @@ void CHC::endVisit(Break const& _break)
 {
 	solAssert(m_breakDest, "");
 	connectBlocks(m_currentBlock, predicate(*m_breakDest));
+
+	// Add an unreachable ghost node to collect unreachable statements after a break.
 	auto breakGhost = createBlock(&_break, PredicateType::FunctionBlock, "break_ghost_");
 	m_currentBlock = predicate(*breakGhost);
 }
@@ -477,6 +479,8 @@ void CHC::endVisit(Continue const& _continue)
 {
 	solAssert(m_continueDest, "");
 	connectBlocks(m_currentBlock, predicate(*m_continueDest));
+
+	// Add an unreachable ghost node to collect unreachable statements after a continue.
 	auto continueGhost = createBlock(&_continue, PredicateType::FunctionBlock, "continue_ghost_");
 	m_currentBlock = predicate(*continueGhost);
 }
@@ -511,6 +515,32 @@ void CHC::endVisit(IndexRangeAccess const& _range)
 	m_context.addAssertion(sliceArray->length() == end - start);
 }
 
+void CHC::endVisit(Return const& _return)
+{
+	SMTEncoder::endVisit(_return);
+
+	connectBlocks(m_currentBlock, predicate(*m_returnDests.back()));
+
+	// Add an unreachable ghost node to collect unreachable statements after a return.
+	auto returnGhost = createBlock(&_return, PredicateType::FunctionBlock, "return_ghost_");
+	m_currentBlock = predicate(*returnGhost);
+}
+
+void CHC::pushInlineFrame(CallableDeclaration const& _callable)
+{
+	m_returnDests.push_back(createBlock(&_callable, PredicateType::FunctionBlock, "return_"));
+}
+
+void CHC::popInlineFrame(CallableDeclaration const& _callable)
+{
+	solAssert(!m_returnDests.empty(), "");
+	auto const& ret = *m_returnDests.back();
+	solAssert(ret.programNode() == &_callable, "");
+	connectBlocks(m_currentBlock, predicate(ret));
+	setCurrentBlock(ret);
+	m_returnDests.pop_back();
+}
+
 void CHC::visitAssert(FunctionCall const& _funCall)
 {
 	auto const& args = _funCall.arguments();
@@ -756,6 +786,7 @@ void CHC::resetContractAnalysis()
 	m_unknownFunctionCallSeen = false;
 	m_breakDest = nullptr;
 	m_continueDest = nullptr;
+	m_returnDests.clear();
 	errorFlag().resetIndex();
 }
 
@@ -806,7 +837,7 @@ set<unsigned> CHC::transactionVerificationTargetsIds(ASTNode const* _txRoot)
 
 SortPointer CHC::sort(FunctionDefinition const& _function)
 {
-	return functionSort(_function, m_currentContract, state());
+	return functionBodySort(_function, m_currentContract, state());
 }
 
 SortPointer CHC::sort(ASTNode const* _node)
@@ -1079,7 +1110,6 @@ smtutil::Expression CHC::predicate(Predicate const& _block)
 		return ::interface(_block, *m_currentContract, m_context);
 	case PredicateType::ConstructorSummary:
 		return constructor(_block, m_context);
-	case PredicateType::FunctionEntry:
 	case PredicateType::FunctionSummary:
 		return smt::function(_block, m_currentContract, m_context);
 	case PredicateType::FunctionBlock:
@@ -1228,7 +1258,7 @@ void CHC::verificationTargetEncountered(
 	connectBlocks(
 		m_currentBlock,
 		predicate(*m_errorDest),
-		currentPathConditions() && _errorCondition && errorFlag().currentValue() == errorId
+		_errorCondition && errorFlag().currentValue() == errorId
 	);
 
 	m_context.addAssertion(errorFlag().currentValue() == previousError);

libsolidity/formal/CHC.h

@@ -83,6 +83,10 @@ private:
 	void endVisit(Break const& _node) override;
 	void endVisit(Continue const& _node) override;
 	void endVisit(IndexRangeAccess const& _node) override;
+	void endVisit(Return const& _node) override;
+
+	void pushInlineFrame(CallableDeclaration const& _callable) override;
+	void popInlineFrame(CallableDeclaration const& _callable) override;
 
 	void visitAssert(FunctionCall const& _funCall);
 	void visitAddMulMod(FunctionCall const& _funCall) override;
@@ -333,6 +337,12 @@ private:
 	/// 2) Constructor summary, if error happens while evaluating base constructor arguments.
 	/// 3) Function summary, if error happens inside a function.
 	Predicate const* m_errorDest = nullptr;
+
+	/// Represents the stack of destinations where a `return` should go.
+	/// This is different from `m_errorDest` above:
+	/// - Constructor initializers and constructor summaries will never be `return` targets because they are artificial.
+	/// - Modifiers also have their own `return` target blocks, whereas they do not have their own error destination.
+	std::vector<Predicate const*> m_returnDests;
 	//@}
 
 	/// CHC solver.

libsolidity/formal/Predicate.h

@@ -35,7 +35,6 @@ enum class PredicateType
 	Interface,
 	NondetInterface,
 	ConstructorSummary,
-	FunctionEntry,
 	FunctionSummary,
 	FunctionBlock,
 	Error,

libsolidity/formal/SMTEncoder.cpp

@@ -152,10 +152,12 @@ void SMTEncoder::visitFunctionOrModifier()
 
 	if (m_modifierDepthStack.back() == static_cast<int>(function.modifiers().size()))
 	{
-		pushPathCondition(currentPathConditions());
 		if (function.isImplemented())
+		{
+			pushInlineFrame(function);
 			function.body().accept(*this);
-		popPathCondition();
+			popInlineFrame(function);
+		}
 	}
 	else
 	{
@@ -192,7 +194,7 @@ void SMTEncoder::inlineModifierInvocation(ModifierInvocation const* _invocation,
 	initializeFunctionCallParameters(*_definition, args);
 
 	pushCallStack({_definition, _invocation});
-	pushPathCondition(currentPathConditions());
+	pushInlineFrame(*_definition);
 	if (auto modifier = dynamic_cast<ModifierDefinition const*>(_definition))
 	{
 		if (modifier->isImplemented())
@@ -205,7 +207,7 @@ void SMTEncoder::inlineModifierInvocation(ModifierInvocation const* _invocation,
 			function->accept(*this);
 		// Functions are popped from the callstack in endVisit(FunctionDefinition)
 	}
-	popPathCondition();
+	popInlineFrame(*_definition);
 }
 
 void SMTEncoder::inlineConstructorHierarchy(ContractDefinition const& _contract)
@@ -289,6 +291,16 @@ bool SMTEncoder::visit(TryCatchClause const& _clause)
 	return false;
 }
 
+void SMTEncoder::pushInlineFrame(CallableDeclaration const&)
+{
+	pushPathCondition(currentPathConditions());
+}
+
+void SMTEncoder::popInlineFrame(CallableDeclaration const&)
+{
+	popPathCondition();
+}
+
 void SMTEncoder::endVisit(VariableDeclarationStatement const& _varDecl)
 {
 	if (_varDecl.declarations().size() != 1)

libsolidity/formal/SMTEncoder.h

@@ -118,6 +118,9 @@ protected:
 	void endVisit(Continue const&) override {}
 	bool visit(TryCatchClause const& _node) override;
 
+	virtual void pushInlineFrame(CallableDeclaration const&);
+	virtual void popInlineFrame(CallableDeclaration const&);
+
 	/// Do not visit subtree if node is a RationalNumber.
 	/// Symbolic _expr is the rational literal.
 	bool shortcutRationalNumber(Expression const& _expr);

test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers.sol

@@ -0,0 +1,26 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+	uint x;
+
+	modifier check() {
+		require(x == 0);
+		_;
+		assert(x == 1); // should fail;
+		assert(x == 0); // should hold;
+	}
+
+	modifier inc() {
+		if (x == 0) {
+			return;
+		}
+		x = x + 1;
+		_;
+	}
+
+	function test() check inc public {
+	}
+}
+// ----
+// Warning 6328: (103-117): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/control_flow/branches_with_return/branches_in_modifiers_2.sol

@@ -0,0 +1,47 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+    uint x;
+
+    function reset_if_overflow() internal postinc {
+        if (x < 10)
+            return;
+        x = 0;
+    }
+
+    modifier postinc() {
+        if (x == 0) {
+            return;
+        }
+        _;
+        x = x + 1;
+    }
+
+    function test() public {
+        if (x == 0) {
+            reset_if_overflow();
+            assert(x == 1); // should fail;
+            assert(x == 0); // should hold;
+            return;
+        }
+        if (x < 10) {
+            uint oldx = x;
+            reset_if_overflow();
+            assert(oldx + 1 == x); // should hold;
+            assert(oldx == x);     // should fail;
+            return;
+        }
+        reset_if_overflow();
+        assert(x == 1); // should hold;
+        assert(x == 0); // should fail;
+    }
+
+    function set(uint _x) public {
+        x = _x;
+    }
+}
+// ----
+// Warning 6328: (384-398): CHC: Assertion violation happens here.
+// Warning 6328: (635-652): CHC: Assertion violation happens here.
+// Warning 6328: (781-795): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructor_state_variable_init.sol

@@ -0,0 +1,41 @@
+pragma experimental SMTChecker;
+
+contract A {
+	int x;
+	constructor (int a) { x = a;}
+}
+
+contract B is A {
+	int y;
+	constructor(int a) A(-a) {
+		if (a > 0) {
+			y = 2;
+			return;
+		}
+		else {
+			y = 3;
+		}
+		y = 4; // overwrites the else branch
+	}
+}
+
+contract C is B {
+	constructor(int a) B(a) {
+		assert(y != 3); // should hold
+		assert(y == 4); // should fail
+		if (a > 0) {
+			assert(x < 0 && y == 2); // should hold
+			assert(x < 0 && y == 4); // should fail
+		}
+		else {
+			assert(x >= 0 && y == 4); // should hold
+			assert(x >= 0 && y == 2); // should fail
+			assert(x > 0); // should fail
+		}
+	}
+}
+// ----
+// Warning 6328: (330-344): CHC: Assertion violation happens here.
+// Warning 6328: (422-445): CHC: Assertion violation happens here.
+// Warning 6328: (522-546): CHC: Assertion violation happens here.
+// Warning 6328: (566-579): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructor_state_variable_init_chain_alternate.sol

@@ -0,0 +1,28 @@
+pragma experimental SMTChecker;
+
+contract A {
+	uint x = 1;
+}
+
+contract B is A {
+	constructor(int a) {
+		if (a > 0) {
+			x = 2;
+			return;
+		}
+		x = 3;
+	}
+}
+
+abstract contract C is B {
+}
+
+contract D is C {
+	constructor(int a) B(a) {
+		assert(a > 0 || x == 3); // should hold
+		assert(a <= 0 || x == 2); // should hold
+		assert(x == 1); // should fail
+	}
+}
+// ----
+// Warning 6328: (319-333): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructor_state_variable_init_diamond.sol

@@ -0,0 +1,70 @@
+pragma experimental SMTChecker;
+
+contract A {
+	int x;
+}
+
+contract B is A {
+	int y;
+	constructor (int a) {
+		if (a >= 0) {
+			y = 1;
+			return;
+		}
+		x = 1;
+		y = 2;
+	}
+}
+
+contract C is A {
+	int z;
+	constructor (int a) {
+		if (a >= 0) {
+			z = 1;
+			return;
+		}
+		x = -1;
+		z = 2;
+	}
+}
+
+contract D1 is B, C {
+	constructor() B(1) C(1) {
+		assert(x == 0); // should hold
+		assert(x == 1); // should fail
+		assert(x == -1); // should fail
+	}
+}
+
+contract D2 is B, C {
+	constructor() B(1) C(-1) {
+		assert(x == 0); // should fail
+		assert(x == 1); // should fail
+		assert(x == -1); // should hold (constructor of C is executed AFTER constructor of B)
+	}
+}
+
+contract D3 is B, C {
+	constructor() B(-1) C(1) {
+		assert(x == 0); // should fail
+		assert(x == 1); // should hold
+		assert(x == -1); // should fail
+	}
+}
+
+contract D4 is B, C {
+	constructor() B(-1) C(-1) {
+		assert(x == 0); // should fail
+		assert(x == 1); // should fail
+		assert(x == -1); // should hold (constructor of C is executed AFTER constructor of B)
+	}
+}
+// ----
+// Warning 6328: (370-384): CHC: Assertion violation happens here.
+// Warning 6328: (403-418): CHC: Assertion violation happens here.
+// Warning 6328: (493-507): CHC: Assertion violation happens here.
+// Warning 6328: (526-540): CHC: Assertion violation happens here.
+// Warning 6328: (703-717): CHC: Assertion violation happens here.
+// Warning 6328: (769-784): CHC: Assertion violation happens here.
+// Warning 6328: (860-874): CHC: Assertion violation happens here.
+// Warning 6328: (893-907): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/control_flow/branches_with_return/constructors.sol

@@ -0,0 +1,31 @@
+pragma experimental SMTChecker;
+
+contract B {
+	int x;
+	constructor(int b) {
+		if (b > 0) {
+			x = 1;
+			return;
+		}
+		else {
+			x = 2;
+			return;
+		}
+		x = 3; // dead code
+	}
+}
+
+contract C is B {
+	constructor(int a) B(a) {
+		assert(a > 0 || x == 2); // should hold
+		assert(a <= 0 || x == 1); // should hold
+		assert(x == 3); // should fail
+		assert(x == 2); // should fail
+		assert(x == 1); // should fail
+	}
+}
+// ----
+// Warning 5740: (152-157): Unreachable code.
+// Warning 6328: (310-324): CHC: Assertion violation happens here.
+// Warning 6328: (343-357): CHC: Assertion violation happens here.
+// Warning 6328: (376-390): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/control_flow/branches_with_return/nested_if.sol

@@ -0,0 +1,26 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+	function test(uint256 a, uint256 b) public pure {
+		assert(nested_if(a,b) != 42); // should hold
+		assert(nested_if(a,b) == 1);  // should fail
+	}
+
+	function nested_if(uint256 a, uint256 b) internal pure returns (uint256) {
+		if (a < 5) {
+			if (b > 1) {
+				return 0;
+			}
+		}
+		if (a == 2 && b == 2) {
+			return 42; // unreachable
+		}
+		else {
+			return 1;
+		}
+	}
+}
+// ----
+// Warning 6328: (147-174): CHC: Assertion violation happens here.
+// Warning 6838: (332-348): BMC: Condition is always false.

test/libsolidity/smtCheckerTests/control_flow/branches_with_return/return_in_both_branches.sol

@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+	function test() public pure {
+		assert(branches(0) == 0);
+		assert(branches(1) == 42);
+	}
+
+	function branches(uint256 a) internal pure returns (uint256) {
+		if (a == 0) {
+			return 0;
+		}
+		else {
+			return 42;
+		}
+		return 1; // dead code
+	}
+}
+// ----
+// Warning 5740: (265-273): Unreachable code.

test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if.sol

@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function test(uint256 a, uint256 b) public pure returns (uint256) {
+		if (a == 0) {
+			return 0;
+		}
+		return b / a; // This division is safe because of the early return in if-block.
+	}
+}

test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if2.sol

@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+	function test(uint256 a) public pure {
+		assert(simple_if(a) == 1); // should fail for a == 0
+	}
+
+	function simple_if(uint256 a) internal pure returns (uint256) {
+		if (a == 0) {
+			return 0;
+		}
+		return 1;
+	}
+}
+// ----
+// Warning 6328: (89-114): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if_array.sol

@@ -0,0 +1,28 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+	uint[] a;
+
+	constructor () {
+		a.push();
+		a.push();
+	}
+
+	function check() public {
+		require(a.length >= 2);
+		require(a[1] == 0);
+		conditional_store();
+		assert(a[1] == 1); // should fail;
+		assert(a[1] == 0); // should hold;
+	}
+
+	function conditional_store() internal {
+		if (a[1] == 0) {
+			return;
+		}
+		a[1] = 1;
+	}
+}
+// ----
+// Warning 6328: (205-222): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if_state_var.sol

@@ -0,0 +1,22 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+	uint x;
+
+	function check() public {
+		require(x == 0);
+		conditional_increment();
+		assert(x == 1); // should fail;
+		assert(x == 0); // should hold;
+	}
+
+	function conditional_increment() internal {
+		if (x == 0) {
+			return;
+		}
+		x = 1;
+	}
+}
+// ----
+// Warning 6328: (132-146): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if_struct.sol

@@ -0,0 +1,25 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+	struct S {
+		uint x;
+	}
+	S s;
+
+	function check() public {
+		require(s.x == 0);
+		conditional_increment();
+		assert(s.x == 1); // should fail;
+		assert(s.x == 0); // should hold;
+	}
+
+	function conditional_increment() internal {
+		if (s.x == 0) {
+			return;
+		}
+		s.x = 1;
+	}
+}
+// ----
+// Warning 6328: (156-172): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if_struct_2.sol

@@ -0,0 +1,25 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+	struct S {
+		uint x;
+	}
+	S s;
+
+	function check() public {
+		require(s.x == 0);
+		conditional_increment();
+		assert(s.x == 1); // should fail;
+		assert(s.x == 0); // should hold;
+	}
+
+	function conditional_increment() internal {
+		if (s.x == 0) {
+			return;
+		}
+		s = S(1);
+	}
+}
+// ----
+// Warning 6328: (156-172): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/control_flow/branches_with_return/simple_if_tuple.sol

@@ -0,0 +1,27 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+	uint x;
+	uint y;
+
+	function check() public {
+		require(x == 0);
+		require(y == 0);
+		conditional_increment();
+		assert(x == 0); // should fail;
+		assert(x == 1); // should fail;
+		assert(x == 2); // should hold;
+	}
+
+	function conditional_increment() internal {
+		if (x == 0) {
+			(x,y) = (2,2);
+			return;
+		}
+		(x,y) = (1,1);
+	}
+}
+// ----
+// Warning 6328: (160-174): CHC: Assertion violation happens here.
+// Warning 6328: (194-208): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/control_flow/branches_with_return/triple_nested_if.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+    uint a;
+    uint b;
+    uint c;
+
+	function test() public view {
+		if (a == 0) {
+			if (b == 0) {
+				if (c == 0) {
+					return;
+				}
+			}
+		}
+		assert(a != 0 || b != 0 || c != 0);
+	}
+}

test/libsolidity/smtCheckerTests/control_flow/return_1.sol

@@ -0,0 +1,22 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function add(uint x, uint y) internal pure returns (uint) {
+		if (y == 0)
+			return x;
+		if (y == 1)
+			return ++x;
+		if (y == 2)
+			return x + 2;
+		return x + y;
+	}
+
+	function f() public pure {
+		assert(add(100, 0) == 100);
+		assert(add(100, 1) == 101);
+		assert(add(100, 2) == 102);
+		assert(add(100, 100) == 200);
+	}
+}
+// ----
+// Warning 2661: (158-161): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

test/libsolidity/smtCheckerTests/control_flow/return_1_fail.sol

@@ -0,0 +1,26 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function add(uint x, uint y) internal pure returns (uint) {
+		if (y == 0)
+			return x;
+		if (y == 1)
+			return ++x;
+		if (y == 2)
+			return x + 2;
+		return x + y;
+	}
+
+	function f() public pure {
+		assert(add(100, 0) != 100);
+		assert(add(100, 1) != 101);
+		assert(add(100, 2) != 102);
+		assert(add(100, 100) != 200);
+	}
+}
+// ----
+// Warning 6328: (244-270): CHC: Assertion violation happens here.
+// Warning 6328: (274-300): CHC: Assertion violation happens here.
+// Warning 6328: (304-330): CHC: Assertion violation happens here.
+// Warning 6328: (334-362): CHC: Assertion violation happens here.
+// Warning 2661: (158-161): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

test/libsolidity/smtCheckerTests/control_flow/return_2.sol

@@ -0,0 +1,31 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint c;
+	function add(uint x, uint y) internal returns (uint) {
+		c = 0xff;
+		if (y == 0)
+			return x;
+		c = 0xffff;
+		if (y == 1)
+			return ++x;
+		c = 0xffffff;
+		if (y == 2)
+			return x + 2;
+		c = 0xffffffff;
+		return x + y;
+	}
+
+	function f() public {
+		assert(add(100, 0) == 100);
+		assert(c == 0xff);
+		assert(add(100, 1) == 101);
+		assert(c == 0xffff);
+		assert(add(100, 2) == 102);
+		assert(c == 0xffffff);
+		assert(add(100, 100) == 200);
+		assert(c == 0xffffffff);
+	}
+}
+// ----
+// Warning 2661: (188-191): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

test/libsolidity/smtCheckerTests/control_flow/return_2_fail.sol

@@ -0,0 +1,39 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint c;
+	function add(uint x, uint y) internal returns (uint) {
+		c = 0xff;
+		if (y == 0)
+			return x;
+		c = 0xffff;
+		if (y == 1)
+			return ++x;
+		c = 0xffffff;
+		if (y == 2)
+			return x + 2;
+		c = 0xffffffff;
+		return x + y;
+	}
+
+	function f() public {
+		assert(add(100, 0) != 100);
+		assert(c != 0xff);
+		assert(add(100, 1) != 101);
+		assert(c != 0xffff);
+		assert(add(100, 2) != 102);
+		assert(c != 0xffffff);
+		assert(add(100, 100) != 200);
+		assert(c != 0xffffffff);
+	}
+}
+// ----
+// Warning 6328: (303-329): CHC: Assertion violation happens here.
+// Warning 6328: (333-350): CHC: Assertion violation happens here.
+// Warning 6328: (354-380): CHC: Assertion violation happens here.
+// Warning 6328: (384-403): CHC: Assertion violation happens here.
+// Warning 6328: (407-433): CHC: Assertion violation happens here.
+// Warning 6328: (437-458): CHC: Assertion violation happens here.
+// Warning 6328: (462-490): CHC: Assertion violation happens here.
+// Warning 6328: (494-517): CHC: Assertion violation happens here.
+// Warning 2661: (188-191): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

test/libsolidity/smtCheckerTests/operators/division_6.sol

@@ -11,4 +11,3 @@ contract C {
 }
 // ----
 // Warning 4984: (160-165): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.
-// Warning 4281: (177-182): CHC: Division by zero happens here.

test/libsolidity/smtCheckerTests/operators/slice.sol

@@ -5,8 +5,8 @@ contract C {
 		require(b[10] == 0xff);
 		assert(bytes(b[10:20]).length == 10);
 		assert(bytes(b[10:20])[0] == 0xff);
-		assert(bytes(b[10:20])[5] == 0xff);
+		// Disabled because of Spacer nondeterminism
+		//assert(bytes(b[10:20])[5] == 0xff);
 	}
 }
 // ----
-// Warning 6328: (198-232): CHC: Assertion violation happens here.