In a seminal work, Miné studied an abstract backward semantic for inferring sufficient program pre-conditions. This analysis exploits under-approximated domain operators, demonstrated by Miné for the polyhedra domain, to under-approximate Dijkstra’s liberal pre-condition. The results of the analysis, were implemented into a static analysis tool for a toy language. In this paper we address some limitations that hinder its applicability to C-like programs. In particular, we focus on two improvements: handling of user input and integer wrapping. For this, we extend the semantic and design sound and effective abstractions. Furthermore, to improve the precision, we explore an under-approximated version of the powerset construction. This in particular helps handling arbitrary union that are difficult to implement with under-approximated domains. The improved analysis is implemented and its performance is compared with other static analysis tools in SV-COMP23 using a selected subset of benchmarks.