ExprData: Better handling of ternary operator

lib/exprengine.cpp

@@ -1613,13 +1613,28 @@ static ExprEngine::ValuePtr executeBinaryOp(const Token *tok, Data &data)
     ExprEngine::ValuePtr v1 = executeExpression(tok->astOperand1(), data);
     ExprEngine::ValuePtr v2;
 
-    if (tok->str() == "?" && tok->astOperand1()->hasKnownIntValue()) {
+    if (tok->str() == "?") {
+        if (tok->astOperand1()->hasKnownIntValue()) {
             if (tok->astOperand1()->getKnownIntValue())
                 v2 = executeExpression(tok->astOperand2()->astOperand1(), data);
             else
                 v2 = executeExpression(tok->astOperand2()->astOperand2(), data);
             call(data.callbacks, tok, v2, &data);
             return v2;
+        }
+
+        Data trueData(data);
+        trueData.addConstraint(v1, true);
+        auto trueValue = simplifyValue(executeExpression(tok->astOperand2()->astOperand1(), trueData));
+
+        Data falseData(data);
+        falseData.addConstraint(v1, false);
+        auto falseValue = simplifyValue(executeExpression(tok->astOperand2()->astOperand2(), falseData));
+
+        auto result = simplifyValue(std::make_shared<ExprEngine::BinOpResult>("?", v1, std::make_shared<ExprEngine::BinOpResult>(":", trueValue, falseValue)));
+        call(data.callbacks, tok, result, &data);
+        return result;
+
     } else if (tok->str() == "&&" || tok->str() == "||") {
         Data data2(data);
         data2.addConstraint(v1, tok->str() == "&&");

test/testexprengine.cpp

@@ -97,6 +97,8 @@ private:
         TEST_CASE(structMember1);
         TEST_CASE(structMember2);
         TEST_CASE(structMember3);
+
+        TEST_CASE(ternaryOperator1);
 #endif
     }
 
@@ -656,6 +658,20 @@ private:
 
         ASSERT_EQUALS(expected, expr(code, "=="));
     }
+
+
+    void ternaryOperator1() {
+        const char code[] = "void foo(signed char x) {\n"
+                            "  x = (x > 0) ? (0==x) : 0;\n"
+                            "}";
+
+        const char expected[] = "(> $1 0)\n"
+                                "(and (>= $1 (- 128)) (<= $1 127))\n"
+                                "(= 0 $1)\n"
+                                "z3::unsat\n";
+
+        ASSERT_EQUALS(expected, expr(code, "=="));
+    }
 };
 
 REGISTER_TEST(TestExprEngine)