Fix ICE on conditions with tuples of rationals

Changelog.md

@@ -8,6 +8,7 @@ Compiler Features:
 Bugfixes:
  * SMTChecker: Fix lack of reporting potential violations when using only the CHC engine.
  * SMTChecker: Fix internal error on conversion from string literal to byte.
+ * SMTChecker: Fix internal error when using tuples of rational literals inside the conditional operator.
  * Code generator: Fix missing creation dependency tracking for abstract contracts.
 
 

libsolidity/formal/SMTEncoder.cpp

@@ -574,8 +574,8 @@ bool SMTEncoder::visit(Conditional const& _op)
 
 	defineExpr(_op, smtutil::Expression::ite(
 		expr(_op.condition()),
-		expr(_op.trueExpression()),
+		expr(_op.trueExpression(), _op.annotation().type),
-		expr(_op.falseExpression())
+		expr(_op.falseExpression(), _op.annotation().type)
 	));
 
 	return false;

libsolidity/formal/SymbolicVariables.cpp

@@ -245,7 +245,25 @@ SymbolicTupleVariable::SymbolicTupleVariable(
 	solAssert(m_sort->kind == Kind::Tuple, "");
 }
 
-vector<SortPointer> const& SymbolicTupleVariable::components()
+smtutil::Expression SymbolicTupleVariable::currentValue(frontend::TypePointer const& _targetType) const
+{
+	if (!_targetType || sort() == smtSort(*_targetType))
+		return SymbolicVariable::currentValue();
+
+	auto thisTuple = dynamic_pointer_cast<TupleSort>(sort());
+	auto otherTuple = dynamic_pointer_cast<TupleSort>(smtSort(*_targetType));
+	solAssert(thisTuple && otherTuple, "");
+	solAssert(thisTuple->components.size() == otherTuple->components.size(), "");
+	vector<smtutil::Expression> args;
+	for (size_t i = 0; i < thisTuple->components.size(); ++i)
+		args.emplace_back(component(i, type(), _targetType));
+	return smtutil::Expression::tuple_constructor(
+		smtutil::Expression(make_shared<smtutil::SortSort>(smtSort(*_targetType)), ""),
+		args
+	);
+}
+
+vector<SortPointer> const& SymbolicTupleVariable::components() const
 {
 	auto tupleSort = dynamic_pointer_cast<TupleSort>(m_sort);
 	solAssert(tupleSort, "");
@@ -256,7 +274,7 @@ smtutil::Expression SymbolicTupleVariable::component(
 	size_t _index,
 	TypePointer _fromType,
 	TypePointer _toType
-)
+) const
 {
 	optional<smtutil::Expression> conversion = symbolicTypeConversion(_fromType, _toType);
 	if (conversion)

libsolidity/formal/SymbolicVariables.h

@@ -225,12 +225,14 @@ public:
 		EncodingContext& _context
 	);
 
-	std::vector<smtutil::SortPointer> const& components();
+	smtutil::Expression currentValue(frontend::TypePointer const& _targetType = TypePointer{}) const override;
+
+	std::vector<smtutil::SortPointer> const& components() const;
 	smtutil::Expression component(
 		size_t _index,
 		TypePointer _fromType = nullptr,
 		TypePointer _toType = nullptr
-	);
+	) const;
 };
 
 /**

test/libsolidity/smtCheckerTests/operators/tuple_rationals_conditional.sol

@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f(bool x) public pure {
+		(uint a, uint b) = x ? (10000000001, 2) : (3, 4);
+		assert(a != 0);
+		assert(b != 0);
+		assert(a % 2 == 1);
+		assert(b % 2 == 0);
+	}
+}