Approximation circuits offer superior performance (speed and area) compared to traditional circuits at the cost of computational accuracy. The accuracy of the results in approximation circuits is evaluated based on several error metrics such as worst-case error, bit-flip error, or error-rate. Several applications have varied requirements in error metrics, i.e., all the error criteria have to be met together at a time, or in combinations. Nevertheless, all applications benefit from improved delay and area. An automated synthesis approach with formal guarantees on error metrics is very helpful in generating circuits that meet these criteria. Furthermore, each of these metrics are independent quantities (value of one metric does not correlate with the other), and automated synthesis can discover opportunities to trade off one or more of the relaxed metrics with a strict requirement on the other, resulting in better performance. In this paper, we present an automatic synthesis approach using And-Inverter Graphs (AIGs) based rewriting that not only improves the performance but also guarantees the bounds of approximation errors introduced. Our synthesis approach is evaluated on a wide range of designs and standard benchmark circuits to show the usefulness and applicability. In particular, we show that our synthesis results are even comparable with the optimization achieved with hand crafted adhoc approximation circuits such as approximation adders in a case study on image compression.